1.1 --- a/src/Pure/General/graph_display.ML	Fri Jan 04 11:21:31 2013 +0100
     1.2 +++ b/src/Pure/General/graph_display.ML	Fri Jan 04 12:33:25 2013 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4    val write_graph_browser: Path.T -> graph -> unit
     1.5    val browserN: string
     1.6    val graphviewN: string
     1.7 -  val graphview_reportN: string
     1.8 +  val active_graphN: string
     1.9    val display_graph: graph -> unit
    1.10  end;
    1.11  
    1.12 @@ -33,12 +33,22 @@
    1.13  
    1.14  val browserN = "browser";
    1.15  val graphviewN = "graphview";
    1.16 -val graphview_reportN = "graphview_report";
    1.17 +val active_graphN = "active_graph";
    1.18  
    1.19 -fun write_graph_browser path (graph: graph) =
    1.20 -  File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents, ...} =>
    1.21 +fun is_browser () =
    1.22 +  (case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of
    1.23 +    SOME m => m = browserN
    1.24 +  | NONE => true);
    1.25 +
    1.26 +
    1.27 +(* encode graph *)
    1.28 +
    1.29 +fun encode_browser (graph: graph) =
    1.30 +  cat_lines (map (fn {name, ID, dir, unfold, path, parents, ...} =>
    1.31      "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
    1.32 -    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") graph));
    1.33 +    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") graph);
    1.34 +
    1.35 +fun write_graph_browser path graph = File.write path (encode_browser graph);
    1.36  
    1.37  
    1.38  val encode_content = YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks;
    1.39 @@ -56,20 +66,18 @@
    1.40  (* display graph *)
    1.41  
    1.42  fun display_graph graph =
    1.43 -  if print_mode_active graphview_reportN then
    1.44 +  if print_mode_active active_graphN then
    1.45      let
    1.46 -      val markup = Active.make_markup Markup.graphviewN {implicit = false, properties = []};
    1.47 -      val ((bg1, bg2), en) = YXML.output_markup_elem markup;
    1.48 -      val graph_yxml = YXML.string_of_body (encode_graphview graph);
    1.49 -    in writeln ("See " ^ bg1 ^ graph_yxml ^ bg2 ^ "graphview" ^ en) end
    1.50 +      val (markup, body) =
    1.51 +        if is_browser () then (Markup.browserN, encode_browser graph)
    1.52 +        else (Markup.graphviewN, YXML.string_of_body (encode_graphview graph));
    1.53 +      val ((bg1, bg2), en) =
    1.54 +        YXML.output_markup_elem (Active.make_markup markup {implicit = false, properties = []});
    1.55 +    in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end
    1.56    else
    1.57      let
    1.58 -      val browser =
    1.59 -        (case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of
    1.60 -          SOME m => m = browserN
    1.61 -        | NONE => true);
    1.62        val (write, tool) =
    1.63 -        if browser then (write_graph_browser, "browser")
    1.64 +        if is_browser () then (write_graph_browser, "browser")
    1.65          else (write_graph_graphview, "graphview");
    1.66  
    1.67        val _ = writeln "Displaying graph ...";

     2.1 --- a/src/Pure/PIDE/markup.ML	Fri Jan 04 11:21:31 2013 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Fri Jan 04 12:33:25 2013 +0100
     2.3 @@ -120,6 +120,7 @@
     2.4    val no_reportN: string val no_report: T
     2.5    val badN: string val bad: T
     2.6    val intensifyN: string val intensify: T
     2.7 +  val browserN: string
     2.8    val graphviewN: string
     2.9    val sendbackN: string
    2.10    val paddingN: string
    2.11 @@ -382,6 +383,7 @@
    2.12  
    2.13  (* active areas *)
    2.14  
    2.15 +val browserN = "browser"
    2.16  val graphviewN = "graphview";
    2.17  
    2.18  val sendbackN = "sendback";

     3.1 --- a/src/Pure/PIDE/markup.scala	Fri Jan 04 11:21:31 2013 +0100
     3.2 +++ b/src/Pure/PIDE/markup.scala	Fri Jan 04 12:33:25 2013 +0100
     3.3 @@ -281,6 +281,7 @@
     3.4  
     3.5    /* active areas */
     3.6  
     3.7 +  val BROWSER = "browser"
     3.8    val GRAPHVIEW = "graphview"
     3.9  
    3.10    val SENDBACK = "sendback"

     4.1 --- a/src/Pure/System/isabelle_process.ML	Fri Jan 04 11:21:31 2013 +0100
     4.2 +++ b/src/Pure/System/isabelle_process.ML	Fri Jan 04 12:33:25 2013 +0100
     4.3 @@ -208,9 +208,9 @@
     4.4  
     4.5  (* init *)
     4.6  
     4.7 -val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
     4.8 -val default_modes2 =
     4.9 -  [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN, Graph_Display.graphview_reportN];
    4.10 +val default_modes1 =
    4.11 +  [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN, Graph_Display.active_graphN];
    4.12 +val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN];
    4.13  
    4.14  fun init rendezvous = ignore (Simple_Thread.fork false (fn () =>
    4.15    let

     5.1 --- a/src/Pure/System/isabelle_system.scala	Fri Jan 04 11:21:31 2013 +0100
     5.2 +++ b/src/Pure/System/isabelle_system.scala	Fri Jan 04 12:33:25 2013 +0100
     5.3 @@ -175,6 +175,8 @@
     5.4      }
     5.5      else jvm_path
     5.6  
     5.7 +  def posix_path(file: JFile): String = posix_path(file.getPath)
     5.8 +
     5.9  
    5.10    /* misc path specifications */
    5.11  
    5.12 @@ -333,7 +335,7 @@
    5.13    {
    5.14      File.with_tmp_file("isabelle_script") { script_file =>
    5.15        File.write(script_file, script)
    5.16 -      val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file.getPath))
    5.17 +      val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file))
    5.18  
    5.19        proc.stdin.close
    5.20        val (_, stdout) = Simple_Thread.future("bash_stdout") { File.read_stream(proc.stdout) }

     6.1 --- a/src/Pure/Tools/build.scala	Fri Jan 04 11:21:31 2013 +0100
     6.2 +++ b/src/Pure/Tools/build.scala	Fri Jan 04 12:33:25 2013 +0100
     6.3 @@ -446,7 +446,7 @@
     6.4      private val env =
     6.5        Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output),
     6.6          (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
     6.7 -          Isabelle_System.posix_path(args_file.getPath))
     6.8 +          Isabelle_System.posix_path(args_file))
     6.9  
    6.10      private val script =
    6.11        if (is_pure(name)) {

     7.1 --- a/src/Tools/jEdit/src/active.scala	Fri Jan 04 11:21:31 2013 +0100
     7.2 +++ b/src/Tools/jEdit/src/active.scala	Fri Jan 04 12:33:25 2013 +0100
     7.3 @@ -43,8 +43,20 @@
     7.4            }
     7.5  
     7.6            if (!snapshot.is_outdated) {
     7.7 +            // FIXME avoid hard-wired stuff
     7.8 +
     7.9              elem match {
    7.10 -              case XML.Elem(Markup(Markup.GRAPHVIEW, Position.Id(exec_id)), body) =>
    7.11 +              case XML.Elem(Markup(Markup.BROWSER, _), body) =>
    7.12 +                default_thread_pool.submit(() =>
    7.13 +                  {
    7.14 +                    val graph_file = File.tmp_file("graph")
    7.15 +                    File.write(graph_file, XML.content(body))
    7.16 +                    Isabelle_System.bash_env(null,
    7.17 +                      Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)),
    7.18 +                      "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &")
    7.19 +                  })
    7.20 +
    7.21 +              case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
    7.22                  default_thread_pool.submit(() =>
    7.23                    {
    7.24                      val graph =

     8.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Jan 04 11:21:31 2013 +0100
     8.2 +++ b/src/Tools/jEdit/src/rendering.scala	Fri Jan 04 12:33:25 2013 +0100
     8.3 @@ -252,7 +252,8 @@
     8.4    }
     8.5  
     8.6  
     8.7 -  private val active_include = Set(Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG)
     8.8 +  private val active_include =
     8.9 +    Set(Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG)
    8.10  
    8.11    def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
    8.12      snapshot.select_markup(range, Some(active_include), command_state =>
    8.13 @@ -261,7 +262,7 @@
    8.14            if !command_state.results.defined(serial) =>
    8.15              Text.Info(snapshot.convert(info_range), elem)
    8.16            case Text.Info(info_range, elem @ XML.Elem(Markup(name, _), _))
    8.17 -          if name == Markup.GRAPHVIEW || name == Markup.SENDBACK =>
    8.18 +          if name == Markup.BROWSER || name == Markup.GRAPHVIEW || name == Markup.SENDBACK =>
    8.19              Text.Info(snapshot.convert(info_range), elem)
    8.20          }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
    8.21