# HG changeset patch
# User wenzelm
# Date 1357299205 -3600
# Node ID 8cfd585b9162d29ac69c5a35d4d0d519d57741ac
# Parent  2af9e4614ba4eb3b840d508414910b723b1b0441
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
clarified print mode "active_graph": allow to switch "browser" vs. "graphview" uniformly;
tuned signature;

diff -r 2af9e4614ba4 -r 8cfd585b9162 src/Pure/General/graph_display.ML
--- a/src/Pure/General/graph_display.ML	Fri Jan 04 11:21:31 2013 +0100
+++ b/src/Pure/General/graph_display.ML	Fri Jan 04 12:33:25 2013 +0100
@@ -13,7 +13,7 @@
   val write_graph_browser: Path.T -> graph -> unit
   val browserN: string
   val graphviewN: string
-  val graphview_reportN: string
+  val active_graphN: string
   val display_graph: graph -> unit
 end;
 
@@ -33,12 +33,22 @@
 
 val browserN = "browser";
 val graphviewN = "graphview";
-val graphview_reportN = "graphview_report";
+val active_graphN = "active_graph";
+
+fun is_browser () =
+  (case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of
+    SOME m => m = browserN
+  | NONE => true);
+
 
-fun write_graph_browser path (graph: graph) =
-  File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents, ...} =>
+(* encode graph *)
+
+fun encode_browser (graph: graph) =
+  cat_lines (map (fn {name, ID, dir, unfold, path, parents, ...} =>
     "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
-    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") graph));
+    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") graph);
+
+fun write_graph_browser path graph = File.write path (encode_browser graph);
 
 
 val encode_content = YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks;
@@ -56,20 +66,18 @@
 (* display graph *)
 
 fun display_graph graph =
-  if print_mode_active graphview_reportN then
+  if print_mode_active active_graphN then
     let
-      val markup = Active.make_markup Markup.graphviewN {implicit = false, properties = []};
-      val ((bg1, bg2), en) = YXML.output_markup_elem markup;
-      val graph_yxml = YXML.string_of_body (encode_graphview graph);
-    in writeln ("See " ^ bg1 ^ graph_yxml ^ bg2 ^ "graphview" ^ en) end
+      val (markup, body) =
+        if is_browser () then (Markup.browserN, encode_browser graph)
+        else (Markup.graphviewN, YXML.string_of_body (encode_graphview graph));
+      val ((bg1, bg2), en) =
+        YXML.output_markup_elem (Active.make_markup markup {implicit = false, properties = []});
+    in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end
   else
     let
-      val browser =
-        (case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of
-          SOME m => m = browserN
-        | NONE => true);
       val (write, tool) =
-        if browser then (write_graph_browser, "browser")
+        if is_browser () then (write_graph_browser, "browser")
         else (write_graph_graphview, "graphview");
 
       val _ = writeln "Displaying graph ...";
diff -r 2af9e4614ba4 -r 8cfd585b9162 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Jan 04 11:21:31 2013 +0100
+++ b/src/Pure/PIDE/markup.ML	Fri Jan 04 12:33:25 2013 +0100
@@ -120,6 +120,7 @@
   val no_reportN: string val no_report: T
   val badN: string val bad: T
   val intensifyN: string val intensify: T
+  val browserN: string
   val graphviewN: string
   val sendbackN: string
   val paddingN: string
@@ -382,6 +383,7 @@
 
 (* active areas *)
 
+val browserN = "browser"
 val graphviewN = "graphview";
 
 val sendbackN = "sendback";
diff -r 2af9e4614ba4 -r 8cfd585b9162 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Jan 04 11:21:31 2013 +0100
+++ b/src/Pure/PIDE/markup.scala	Fri Jan 04 12:33:25 2013 +0100
@@ -281,6 +281,7 @@
 
   /* active areas */
 
+  val BROWSER = "browser"
   val GRAPHVIEW = "graphview"
 
   val SENDBACK = "sendback"
diff -r 2af9e4614ba4 -r 8cfd585b9162 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Fri Jan 04 11:21:31 2013 +0100
+++ b/src/Pure/System/isabelle_process.ML	Fri Jan 04 12:33:25 2013 +0100
@@ -208,9 +208,9 @@
 
 (* init *)
 
-val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
-val default_modes2 =
-  [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN, Graph_Display.graphview_reportN];
+val default_modes1 =
+  [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN, Graph_Display.active_graphN];
+val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN];
 
 fun init rendezvous = ignore (Simple_Thread.fork false (fn () =>
   let
diff -r 2af9e4614ba4 -r 8cfd585b9162 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Fri Jan 04 11:21:31 2013 +0100
+++ b/src/Pure/System/isabelle_system.scala	Fri Jan 04 12:33:25 2013 +0100
@@ -175,6 +175,8 @@
     }
     else jvm_path
 
+  def posix_path(file: JFile): String = posix_path(file.getPath)
+
 
   /* misc path specifications */
 
@@ -333,7 +335,7 @@
   {
     File.with_tmp_file("isabelle_script") { script_file =>
       File.write(script_file, script)
-      val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file.getPath))
+      val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file))
 
       proc.stdin.close
       val (_, stdout) = Simple_Thread.future("bash_stdout") { File.read_stream(proc.stdout) }
diff -r 2af9e4614ba4 -r 8cfd585b9162 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Jan 04 11:21:31 2013 +0100
+++ b/src/Pure/Tools/build.scala	Fri Jan 04 12:33:25 2013 +0100
@@ -446,7 +446,7 @@
     private val env =
       Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output),
         (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
-          Isabelle_System.posix_path(args_file.getPath))
+          Isabelle_System.posix_path(args_file))
 
     private val script =
       if (is_pure(name)) {
diff -r 2af9e4614ba4 -r 8cfd585b9162 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Fri Jan 04 11:21:31 2013 +0100
+++ b/src/Tools/jEdit/src/active.scala	Fri Jan 04 12:33:25 2013 +0100
@@ -43,8 +43,20 @@
           }
 
           if (!snapshot.is_outdated) {
+            // FIXME avoid hard-wired stuff
+
             elem match {
-              case XML.Elem(Markup(Markup.GRAPHVIEW, Position.Id(exec_id)), body) =>
+              case XML.Elem(Markup(Markup.BROWSER, _), body) =>
+                default_thread_pool.submit(() =>
+                  {
+                    val graph_file = File.tmp_file("graph")
+                    File.write(graph_file, XML.content(body))
+                    Isabelle_System.bash_env(null,
+                      Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)),
+                      "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &")
+                  })
+
+              case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
                 default_thread_pool.submit(() =>
                   {
                     val graph =
diff -r 2af9e4614ba4 -r 8cfd585b9162 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Fri Jan 04 11:21:31 2013 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Jan 04 12:33:25 2013 +0100
@@ -252,7 +252,8 @@
   }
 
 
-  private val active_include = Set(Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG)
+  private val active_include =
+    Set(Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG)
 
   def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
     snapshot.select_markup(range, Some(active_include), command_state =>
@@ -261,7 +262,7 @@
           if !command_state.results.defined(serial) =>
             Text.Info(snapshot.convert(info_range), elem)
           case Text.Info(info_range, elem @ XML.Elem(Markup(name, _), _))
-          if name == Markup.GRAPHVIEW || name == Markup.SENDBACK =>
+          if name == Markup.BROWSER || name == Markup.GRAPHVIEW || name == Markup.SENDBACK =>
             Text.Info(snapshot.convert(info_range), elem)
         }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }