From 14a84664583048445c098122c871cc4ef261db42 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 3 Sep 2024 14:58:10 +0200 Subject: [PATCH] style --- ImportGraph/Cli.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean index 40921a2..bbbbf86 100644 --- a/ImportGraph/Cli.lean +++ b/ImportGraph/Cli.lean @@ -17,8 +17,10 @@ open ImportGraph /-- Write an import graph, represented as a `NameMap (Array Name)` to the ".dot" graph format. * Nodes in the `unused` set will be shaded light gray. -* Nodes which start with the `markedModule` and edges into them will be highlighted in green. -* Nodes in `directDeps` are marked with a green border and green text. +* If `markedModule` is provided: + * Nodes which start with the `markedModule` will be highlighted in green and drawn closer together. + * Edges from `directDeps` into the module are highlighted in green + * Nodes in `directDeps` are marked with a green border and green text. -/ def asDotGraph (graph : NameMap (Array Name))