more explicit HTML.symbols;
authorwenzelm
Sat Oct 10 16:21:34 2015 +0200 (2015-10-10)
changeset 61381ddca85598c65
parent 61380 3907f20bef8c
child 61382 efac889fccbc
more explicit HTML.symbols;
tuned signature;
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/resources.ML
src/Pure/PIDE/session.ML
src/Pure/PIDE/session.scala
src/Pure/Thy/html.ML
src/Pure/Thy/present.ML
src/Pure/Thy/thy_info.ML
src/Pure/Tools/build.ML
     1.1 --- a/src/Pure/PIDE/protocol.ML	Fri Oct 09 21:20:43 2015 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.ML	Sat Oct 10 16:21:34 2015 +0200
     1.3 @@ -12,13 +12,6 @@
     1.4      (fn args => List.app writeln args);
     1.5  
     1.6  val _ =
     1.7 -  Isabelle_Process.protocol_command "Prover.init_symbols"
     1.8 -    (fn [codes_yxml] =>
     1.9 -      YXML.parse_body codes_yxml
    1.10 -      |> let open XML.Decode in list (pair string int) end
    1.11 -      |> HTML.init_symbols);
    1.12 -
    1.13 -val _ =
    1.14    Isabelle_Process.protocol_command "Prover.options"
    1.15      (fn [options_yxml] =>
    1.16        let val options = Options.decode (YXML.parse_body options_yxml) in
     2.1 --- a/src/Pure/PIDE/protocol.scala	Fri Oct 09 21:20:43 2015 +0200
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Oct 10 16:21:34 2015 +0200
     2.3 @@ -308,19 +308,6 @@
     2.4    def protocol_command(name: String, args: String*): Unit
     2.5  
     2.6  
     2.7 -  /* symbols */
     2.8 -
     2.9 -  def init_symbols(): Unit =
    2.10 -  {
    2.11 -    val codes_yxml =
    2.12 -    {
    2.13 -      import XML.Encode._
    2.14 -      YXML.string_of_body(list(pair(string, int))(Symbol.codes))
    2.15 -    }
    2.16 -    protocol_command("Prover.init_symbols", codes_yxml)
    2.17 -  }
    2.18 -
    2.19 -
    2.20    /* options */
    2.21  
    2.22    def options(opts: Options): Unit =
    2.23 @@ -425,6 +412,9 @@
    2.24  
    2.25    def build_theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
    2.26    {
    2.27 +    val symbol_codes_yxml =
    2.28 +    { import XML.Encode._
    2.29 +      YXML.string_of_body(list(pair(string, int))(Symbol.codes)) }
    2.30      val theories_yxml =
    2.31      { import XML.Encode._
    2.32        YXML.string_of_body(list(pair(Options.encode, list(Path.encode)))(theories)) }
     3.1 --- a/src/Pure/PIDE/resources.ML	Fri Oct 09 21:20:43 2015 +0200
     3.2 +++ b/src/Pure/PIDE/resources.ML	Sat Oct 10 16:21:34 2015 +0200
     3.3 @@ -17,8 +17,9 @@
     3.4    val provide_parse_files: string -> (theory -> Token.file list * theory) parser
     3.5    val loaded_files_current: theory -> bool
     3.6    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
     3.7 -  val load_thy: bool -> (Toplevel.transition -> Time.time option) -> int -> Path.T ->
     3.8 -    Thy_Header.header -> Position.T -> string -> theory list -> theory * (unit -> unit) * int
     3.9 +  val load_thy: bool -> HTML.symbols -> (Toplevel.transition -> Time.time option) -> int ->
    3.10 +    Path.T -> Thy_Header.header -> Position.T -> string -> theory list ->
    3.11 +    theory * (unit -> unit) * int
    3.12  end;
    3.13  
    3.14  structure Resources: RESOURCES =
    3.15 @@ -145,7 +146,7 @@
    3.16      val thy = Toplevel.end_theory end_pos end_state;
    3.17    in (results, thy) end;
    3.18  
    3.19 -fun load_thy document last_timing update_time master_dir header text_pos text parents =
    3.20 +fun load_thy document symbols last_timing update_time master_dir header text_pos text parents =
    3.21    let
    3.22      val (name, _) = #name header;
    3.23      val keywords =
    3.24 @@ -159,7 +160,7 @@
    3.25      fun init () =
    3.26        begin_theory master_dir header parents
    3.27        |> Present.begin_theory update_time
    3.28 -        (fn () => implode (map (HTML.present_span keywords) spans));
    3.29 +        (fn () => implode (map (HTML.present_span symbols keywords) spans));
    3.30  
    3.31      val (results, thy) =
    3.32        cond_timeit true ("theory " ^ quote name)
     4.1 --- a/src/Pure/PIDE/session.ML	Fri Oct 09 21:20:43 2015 +0200
     4.2 +++ b/src/Pure/PIDE/session.ML	Sat Oct 10 16:21:34 2015 +0200
     4.3 @@ -9,7 +9,7 @@
     4.4    val get_name: unit -> string
     4.5    val welcome: unit -> string
     4.6    val get_keywords: unit -> Keyword.keywords
     4.7 -  val init: bool -> bool -> Path.T -> string -> string -> (string * string) list ->
     4.8 +  val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
     4.9      (Path.T * Path.T) list -> Path.T -> string -> string * string -> bool -> unit
    4.10    val shutdown: unit -> unit
    4.11    val finish: unit -> unit
    4.12 @@ -44,7 +44,7 @@
    4.13  
    4.14  (* init *)
    4.15  
    4.16 -fun init build info info_path doc doc_output doc_variants doc_files graph_file
    4.17 +fun init symbols build info info_path doc doc_output doc_variants doc_files graph_file
    4.18      parent (chapter, name) verbose =
    4.19    if get_name () <> parent orelse not (! session_finished) then
    4.20      error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
    4.21 @@ -53,7 +53,7 @@
    4.22        val _ = session := {chapter = chapter, name = name};
    4.23        val _ = session_finished := false;
    4.24      in
    4.25 -      Present.init build info info_path (if doc = "false" then "" else doc)
    4.26 +      Present.init symbols build info info_path (if doc = "false" then "" else doc)
    4.27          doc_output doc_variants doc_files graph_file (chapter, name) verbose
    4.28      end;
    4.29  
     5.1 --- a/src/Pure/PIDE/session.scala	Fri Oct 09 21:20:43 2015 +0200
     5.2 +++ b/src/Pure/PIDE/session.scala	Sat Oct 10 16:21:34 2015 +0200
     5.3 @@ -494,7 +494,6 @@
     5.4                accumulate(state_id, output.message)
     5.5  
     5.6              case _ if output.is_init =>
     5.7 -              prover.get.init_symbols()
     5.8                phase = Session.Ready
     5.9  
    5.10              case Markup.Return_Code(rc) if output.is_exit =>
     6.1 --- a/src/Pure/Thy/html.ML	Fri Oct 09 21:20:43 2015 +0200
     6.2 +++ b/src/Pure/Thy/html.ML	Sat Oct 10 16:21:34 2015 +0200
     6.3 @@ -6,23 +6,16 @@
     6.4  
     6.5  signature HTML =
     6.6  sig
     6.7 -  val reset_symbols: unit -> unit
     6.8 -  val init_symbols: (string * int) list -> unit
     6.9 -  val present_span: Keyword.keywords -> Command_Span.span -> Output.output
    6.10 +  type symbols
    6.11 +  val make_symbols: (string * int) list -> symbols
    6.12 +  val no_symbols: symbols
    6.13 +  val present_span: symbols -> Keyword.keywords -> Command_Span.span -> Output.output
    6.14    type text = string
    6.15 -  val plain: string -> text
    6.16 -  val name: string -> text
    6.17 -  val keyword: string -> text
    6.18 -  val command: string -> text
    6.19 -  val href_name: string -> text -> text
    6.20 -  val href_path: Url.T -> text -> text
    6.21 -  val href_opt_path: Url.T option -> text -> text
    6.22 -  val para: text -> text
    6.23 -  val begin_document: string -> text
    6.24 +  val begin_document: symbols -> string -> text
    6.25    val end_document: text
    6.26 -  val begin_session_index: string -> Url.T -> (Url.T * string) list -> text
    6.27 -  val theory_entry: Url.T * string -> text
    6.28 -  val theory: string -> (Url.T option * string) list -> text -> text
    6.29 +  val begin_session_index: symbols -> string -> Url.T -> (Url.T * string) list -> text
    6.30 +  val theory_entry: symbols -> Url.T * string -> text
    6.31 +  val theory: symbols -> string -> (Url.T option * string) list -> text -> text
    6.32  end;
    6.33  
    6.34  structure HTML: HTML =
    6.35 @@ -38,70 +31,66 @@
    6.36  
    6.37  (* symbol output *)
    6.38  
    6.39 +abstype symbols = Symbols of string Symtab.table
    6.40 +with
    6.41 +
    6.42 +fun make_symbols codes =
    6.43 +  let
    6.44 +    val mapping =
    6.45 +      map (apsnd (fn c => "&#" ^ Markup.print_int c ^ ";")) codes @
    6.46 +       [("'", "&#39;"),
    6.47 +        ("\\<^bsub>", hidden "&#8664;" ^ "<sub>"),
    6.48 +        ("\\<^esub>", hidden "&#8665;" ^ "</sub>"),
    6.49 +        ("\\<^bsup>", hidden "&#8663;" ^ "<sup>"),
    6.50 +        ("\\<^esup>", hidden "&#8662;" ^ "</sup>")];
    6.51 +  in Symbols (fold Symtab.update mapping Symtab.empty) end;
    6.52 +
    6.53 +val no_symbols = make_symbols [];
    6.54 +
    6.55 +fun output_sym (Symbols tab) s =
    6.56 +  if Symbol.is_raw s then Symbol.decode_raw s
    6.57 +  else
    6.58 +    (case Symtab.lookup tab s of
    6.59 +      SOME x => x
    6.60 +    | NONE => XML.text s);
    6.61 +
    6.62 +end;
    6.63 +
    6.64  local
    6.65  
    6.66 -val symbols =
    6.67 -  Synchronized.var "HTML.symbols" (NONE: (int * string) Symtab.table option);
    6.68 -
    6.69 -fun output_sym s =
    6.70 -  if Symbol.is_raw s then (1, Symbol.decode_raw s)
    6.71 -  else
    6.72 -    (case Synchronized.value symbols of
    6.73 -      SOME tab =>
    6.74 -        (case Symtab.lookup tab s of
    6.75 -          SOME x => x
    6.76 -        | NONE => (size s, XML.text s))
    6.77 -    | NONE => raise Fail "Missing HTML.init_symbols: cannot output symbols");
    6.78 -
    6.79 -fun output_markup (bg, en) s1 s2 =
    6.80 -  let val (n, txt) = output_sym s2
    6.81 -  in (n, hidden s1 ^ enclose bg en txt) end;
    6.82 +fun output_markup (bg, en) symbols s1 s2 =
    6.83 +  hidden s1 ^ enclose bg en (output_sym symbols s2);
    6.84  
    6.85  val output_sub = output_markup ("<sub>", "</sub>");
    6.86  val output_sup = output_markup ("<sup>", "</sup>");
    6.87  val output_bold = output_markup (span "bold");
    6.88  
    6.89 -fun output_syms [] (result, width) = (implode (rev result), width)
    6.90 -  | output_syms (s1 :: rest) (result, width) =
    6.91 +fun output_syms _ [] result = implode (rev result)
    6.92 +  | output_syms symbols (s1 :: rest) result =
    6.93        let
    6.94          val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss));
    6.95 -        val ((w, s), r) =
    6.96 -          if s1 = "\\<^sub>" then (output_sub "&#8681;" s2, ss)
    6.97 -          else if s1 = "\\<^sup>" then (output_sup "&#8679;" s2, ss)
    6.98 -          else if s1 = "\\<^bold>" then (output_bold "&#10073;" s2, ss)
    6.99 -          else (output_sym s1, rest);
   6.100 -      in output_syms r (s :: result, width + w) end;
   6.101 +        val (s, r) =
   6.102 +          if s1 = "\\<^sub>" then (output_sub symbols "&#8681;" s2, ss)
   6.103 +          else if s1 = "\\<^sup>" then (output_sup symbols "&#8679;" s2, ss)
   6.104 +          else if s1 = "\\<^bold>" then (output_bold symbols "&#10073;" s2, ss)
   6.105 +          else (output_sym symbols s1, rest);
   6.106 +      in output_syms symbols r (s :: result) end;
   6.107  
   6.108  in
   6.109  
   6.110 -fun output_width str = output_syms (Symbol.explode str) ([], 0);
   6.111 -val output = #1 o output_width;
   6.112 -
   6.113 -fun reset_symbols () = Synchronized.change symbols (K NONE);
   6.114 -
   6.115 -fun init_symbols codes =
   6.116 -  let
   6.117 -    val mapping =
   6.118 -      map (fn (s, c) => (s, (Symbol.length [s], "&#" ^ Markup.print_int c ^ ";"))) codes @
   6.119 -       [("", (0, "")),
   6.120 -        ("'", (1, "&#39;")),
   6.121 -        ("\\<^bsub>", (0, hidden "&#8664;" ^ "<sub>")),
   6.122 -        ("\\<^esub>", (0, hidden "&#8665;" ^ "</sub>")),
   6.123 -        ("\\<^bsup>", (0, hidden "&#8663;" ^ "<sup>")),
   6.124 -        ("\\<^esup>", (0, hidden "&#8662;" ^ "</sup>"))];
   6.125 -  in Synchronized.change symbols (K (SOME (fold Symtab.update mapping Symtab.empty))) end;
   6.126 +fun output symbols str = output_syms symbols (Symbol.explode str) [];
   6.127  
   6.128  end;
   6.129  
   6.130  
   6.131  (* presentation *)
   6.132  
   6.133 -fun present_token keywords tok =
   6.134 -  fold_rev (uncurry enclose o span o #1)
   6.135 -    (Token.markups keywords tok) (output (Token.unparse tok));
   6.136 -
   6.137 -fun present_span keywords =
   6.138 -  implode o map (present_token keywords) o Command_Span.content;
   6.139 +fun present_span symbols keywords =
   6.140 +  let
   6.141 +    fun present_token tok =
   6.142 +      fold_rev (uncurry enclose o span o #1)
   6.143 +        (Token.markups keywords tok) (output symbols (Token.unparse tok));
   6.144 +  in implode o map present_token o Command_Span.content end;
   6.145  
   6.146  
   6.147  
   6.148 @@ -112,10 +101,9 @@
   6.149  
   6.150  (* atoms *)
   6.151  
   6.152 -val plain = output;
   6.153 -val name = enclose "<span class=\"name\">" "</span>" o output;
   6.154 -val keyword = enclose "<span class=\"keyword\">" "</span>" o output;
   6.155 -val command = enclose "<span class=\"command\">" "</span>" o output;
   6.156 +val name = enclose "<span class=\"name\">" "</span>" oo output;
   6.157 +val keyword = enclose "<span class=\"keyword\">" "</span>" oo output;
   6.158 +val command = enclose "<span class=\"command\">" "</span>" oo output;
   6.159  
   6.160  
   6.161  (* misc *)
   6.162 @@ -131,41 +119,42 @@
   6.163  
   6.164  (* document *)
   6.165  
   6.166 -fun begin_document title =
   6.167 +fun begin_document symbols title =
   6.168    "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n\
   6.169    \<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \
   6.170    \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\
   6.171    \<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\
   6.172    \<head>\n\
   6.173    \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n\
   6.174 -  \<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
   6.175 +  \<title>" ^ output symbols (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
   6.176    \<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n\
   6.177    \</head>\n\
   6.178    \\n\
   6.179    \<body>\n\
   6.180    \<div class=\"head\">\
   6.181 -  \<h1>" ^ plain title ^ "</h1>\n";
   6.182 +  \<h1>" ^ output symbols title ^ "</h1>\n";
   6.183  
   6.184  val end_document = "\n</div>\n</body>\n</html>\n";
   6.185  
   6.186  
   6.187  (* session index *)
   6.188  
   6.189 -fun begin_session_index session graph docs =
   6.190 -  begin_document ("Session " ^ plain session) ^
   6.191 +fun begin_session_index symbols session graph docs =
   6.192 +  begin_document symbols ("Session " ^ output symbols session) ^
   6.193    para ("View " ^ href_path graph "theory dependencies" ^
   6.194      implode (map (fn (p, name) => "<br/>\nView " ^ href_path p name) docs)) ^
   6.195    "\n</div>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
   6.196  
   6.197 -fun theory_entry (p, s) = "<li>" ^ href_path p (plain s) ^ "</li>\n";
   6.198 +fun theory_entry symbols (p, s) = "<li>" ^ href_path p (output symbols s) ^ "</li>\n";
   6.199  
   6.200  
   6.201  (* theory *)
   6.202  
   6.203 -fun theory A Bs txt =
   6.204 -  begin_document ("Theory " ^ A) ^ "\n" ^
   6.205 -  command "theory" ^ " " ^ name A ^ "<br/>\n" ^
   6.206 -  keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs) ^
   6.207 +fun theory symbols A Bs txt =
   6.208 +  begin_document symbols ("Theory " ^ A) ^ "\n" ^
   6.209 +  command symbols "theory" ^ " " ^ name symbols A ^ "<br/>\n" ^
   6.210 +  keyword symbols "imports" ^ " " ^
   6.211 +    space_implode " " (map (uncurry href_opt_path o apsnd (name symbols)) Bs) ^
   6.212    "<br/>\n" ^
   6.213    enclose "\n</div>\n<div class=\"source\">\n<pre class=\"source\">" "</pre>\n" txt ^
   6.214    end_document;
     7.1 --- a/src/Pure/Thy/present.ML	Fri Oct 09 21:20:43 2015 +0200
     7.2 +++ b/src/Pure/Thy/present.ML	Sat Oct 10 16:21:34 2015 +0200
     7.3 @@ -10,7 +10,7 @@
     7.4    val session_graph: string -> (string -> bool) -> theory -> Graph_Display.entry list
     7.5    val document_enabled: string -> bool
     7.6    val document_variants: string -> (string * string) list
     7.7 -  val init: bool -> bool -> Path.T -> string -> string -> (string * string) list ->
     7.8 +  val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
     7.9      (Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit
    7.10    val finish: unit -> unit
    7.11    val theory_output: string -> string -> unit
    7.12 @@ -138,15 +138,15 @@
    7.13  (* session_info *)
    7.14  
    7.15  type session_info =
    7.16 -  {name: string, chapter: string, info_path: Path.T, info: bool, doc_format: string,
    7.17 -    doc_output: Path.T option, doc_files: (Path.T * Path.T) list, graph_file: Path.T,
    7.18 -    documents: (string * string) list, verbose: bool, readme: Path.T option};
    7.19 +  {symbols: HTML.symbols, name: string, chapter: string, info_path: Path.T, info: bool,
    7.20 +    doc_format: string, doc_output: Path.T option, doc_files: (Path.T * Path.T) list,
    7.21 +    graph_file: Path.T, documents: (string * string) list, verbose: bool, readme: Path.T option};
    7.22  
    7.23  fun make_session_info
    7.24 -  (name, chapter, info_path, info, doc_format, doc_output, doc_files,
    7.25 +  (symbols, name, chapter, info_path, info, doc_format, doc_output, doc_files,
    7.26      graph_file, documents, verbose, readme) =
    7.27 -  {name = name, chapter = chapter, info_path = info_path, info = info, doc_format = doc_format,
    7.28 -    doc_output = doc_output, doc_files = doc_files, graph_file = graph_file,
    7.29 +  {symbols = symbols, name = name, chapter = chapter, info_path = info_path, info = info,
    7.30 +    doc_format = doc_format, doc_output = doc_output, doc_files = doc_files, graph_file = graph_file,
    7.31      documents = documents, verbose = verbose, readme = readme}: session_info;
    7.32  
    7.33  
    7.34 @@ -181,7 +181,7 @@
    7.35  
    7.36  (* init session *)
    7.37  
    7.38 -fun init build info info_path doc document_output doc_variants doc_files graph_file
    7.39 +fun init symbols build info info_path doc document_output doc_variants doc_files graph_file
    7.40      (chapter, name) verbose =
    7.41    if not build andalso not info andalso doc = "" then
    7.42      (Synchronized.change browser_info (K empty_browser_info); session_info := NONE)
    7.43 @@ -204,10 +204,10 @@
    7.44            map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
    7.45      in
    7.46        session_info :=
    7.47 -        SOME (make_session_info (name, chapter, info_path, info, doc,
    7.48 +        SOME (make_session_info (symbols, name, chapter, info_path, info, doc,
    7.49            doc_output, doc_files, graph_file, documents, verbose, readme));
    7.50        Synchronized.change browser_info (K empty_browser_info);
    7.51 -      add_html_index (0, HTML.begin_session_index name (Url.File session_graph_path) docs)
    7.52 +      add_html_index (0, HTML.begin_session_index symbols name (Url.File session_graph_path) docs)
    7.53      end;
    7.54  
    7.55  
    7.56 @@ -320,7 +320,7 @@
    7.57    end;
    7.58  
    7.59  fun begin_theory update_time mk_text thy =
    7.60 -  with_session_info thy (fn {name = session_name, chapter, ...} =>
    7.61 +  with_session_info thy (fn {symbols, name = session_name, chapter, ...} =>
    7.62      let
    7.63        val name = Context.theory_name thy;
    7.64        val parents = Theory.parents_of thy;
    7.65 @@ -328,10 +328,10 @@
    7.66        val parent_specs = parents |> map (fn parent =>
    7.67          (Option.map Url.File (theory_link (chapter, session_name) parent),
    7.68            (Context.theory_name parent)));
    7.69 -      val html_source = HTML.theory name parent_specs (mk_text ());
    7.70 +      val html_source = HTML.theory symbols name parent_specs (mk_text ());
    7.71      in
    7.72        init_theory_info name (make_theory_info ("", html_source));
    7.73 -      add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
    7.74 +      add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name));
    7.75        add_tex_index (update_time, Latex.theory_entry name);
    7.76        Browser_Info.put {chapter = chapter, name = session_name} thy
    7.77      end);
     8.1 --- a/src/Pure/Thy/thy_info.ML	Fri Oct 09 21:20:43 2015 +0200
     8.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Oct 10 16:21:34 2015 +0200
     8.3 @@ -14,8 +14,10 @@
     8.4    val master_directory: string -> Path.T
     8.5    val remove_thy: string -> unit
     8.6    val use_theories:
     8.7 -    {document: bool, last_timing: Toplevel.transition -> Time.time option, master_dir: Path.T} ->
     8.8 -    (string * Position.T) list -> unit
     8.9 +    {document: bool,
    8.10 +     symbols: HTML.symbols,
    8.11 +     last_timing: Toplevel.transition -> Time.time option,
    8.12 +     master_dir: Path.T} -> (string * Position.T) list -> unit
    8.13    val use_thys: (string * Position.T) list -> unit
    8.14    val use_thy: string * Position.T -> unit
    8.15    val script_thy: Position.T -> string -> theory -> theory
    8.16 @@ -237,7 +239,8 @@
    8.17  fun required_by _ [] = ""
    8.18    | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
    8.19  
    8.20 -fun load_thy document last_timing initiators update_time deps text (name, pos) keywords parents =
    8.21 +fun load_thy document symbols last_timing
    8.22 +    initiators update_time deps text (name, pos) keywords parents =
    8.23    let
    8.24      val _ = remove_thy name;
    8.25      val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
    8.26 @@ -256,7 +259,7 @@
    8.27  
    8.28      val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
    8.29      val (theory, present, weight) =
    8.30 -      Resources.load_thy document last_timing update_time dir header text_pos text
    8.31 +      Resources.load_thy document symbols last_timing update_time dir header text_pos text
    8.32          (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
    8.33      fun commit () = update_thy deps theory;
    8.34    in
    8.35 @@ -283,9 +286,9 @@
    8.36  
    8.37  in
    8.38  
    8.39 -fun require_thys document last_timing initiators dir strs tasks =
    8.40 -      fold_map (require_thy document last_timing initiators dir) strs tasks |>> forall I
    8.41 -and require_thy document last_timing initiators dir (str, require_pos) tasks =
    8.42 +fun require_thys document symbols last_timing initiators dir strs tasks =
    8.43 +      fold_map (require_thy document symbols last_timing initiators dir) strs tasks |>> forall I
    8.44 +and require_thy document symbols last_timing initiators dir (str, require_pos) tasks =
    8.45    let
    8.46      val path = Path.expand (Path.explode str);
    8.47      val name = Path.implode (Path.base path);
    8.48 @@ -315,7 +318,7 @@
    8.49  
    8.50            val parents = map (base_name o #1) imports;
    8.51            val (parents_current, tasks') =
    8.52 -            require_thys document last_timing (name :: initiators)
    8.53 +            require_thys document symbols last_timing (name :: initiators)
    8.54                (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
    8.55  
    8.56            val all_current = current andalso parents_current;
    8.57 @@ -328,7 +331,7 @@
    8.58                    let
    8.59                      val update_time = serial ();
    8.60                      val load =
    8.61 -                      load_thy document last_timing initiators update_time dep
    8.62 +                      load_thy document symbols last_timing initiators update_time dep
    8.63                          text (name, theory_pos) keywords;
    8.64                    in Task (node_name, parents, load) end);
    8.65  
    8.66 @@ -341,10 +344,14 @@
    8.67  
    8.68  (* use_thy *)
    8.69  
    8.70 -fun use_theories {document, last_timing, master_dir} imports =
    8.71 -  schedule_tasks (snd (require_thys document last_timing [] master_dir imports String_Graph.empty));
    8.72 +fun use_theories {document, symbols, last_timing, master_dir} imports =
    8.73 +  schedule_tasks
    8.74 +    (snd (require_thys document symbols last_timing [] master_dir imports String_Graph.empty));
    8.75  
    8.76 -val use_thys = use_theories {document = false, last_timing = K NONE, master_dir = Path.current};
    8.77 +val use_thys =
    8.78 +  use_theories
    8.79 +    {document = false, symbols = HTML.no_symbols, last_timing = K NONE, master_dir = Path.current};
    8.80 +
    8.81  val use_thy = use_thys o single;
    8.82  
    8.83  
     9.1 --- a/src/Pure/Tools/build.ML	Fri Oct 09 21:20:43 2015 +0200
     9.2 +++ b/src/Pure/Tools/build.ML	Sat Oct 10 16:21:34 2015 +0200
     9.3 @@ -97,7 +97,7 @@
     9.4  
     9.5  (* build *)
     9.6  
     9.7 -fun build_theories last_timing master_dir (options, thys) =
     9.8 +fun build_theories symbols last_timing master_dir (options, thys) =
     9.9    let
    9.10      val condition = space_explode "," (Options.string options "condition");
    9.11      val conds = filter_out (can getenv_strict) condition;
    9.12 @@ -106,6 +106,7 @@
    9.13        (Options.set_default options;
    9.14          (Thy_Info.use_theories {
    9.15            document = Present.document_enabled (Options.string options "document"),
    9.16 +          symbols = symbols,
    9.17            last_timing = last_timing,
    9.18            master_dir = master_dir}
    9.19          |> Unsynchronized.setmp print_mode
    9.20 @@ -133,12 +134,14 @@
    9.21                  ((list (pair Options.decode (list (string #> rpair Position.none)))))))))))))))
    9.22            end;
    9.23  
    9.24 -      val _ = HTML.init_symbols symbol_codes;
    9.25 +      val symbols = HTML.make_symbols symbol_codes;
    9.26        val _ = Options.set_default options;
    9.27  
    9.28        val _ = writeln ("\fSession.name = " ^ name);
    9.29        val _ =
    9.30 -        Session.init do_output
    9.31 +        Session.init
    9.32 +          symbols
    9.33 +          do_output
    9.34            (Options.bool options "browser_info")
    9.35            (Path.explode browser_info)
    9.36            (Options.string options "document")
    9.37 @@ -153,7 +156,7 @@
    9.38  
    9.39        val res1 =
    9.40          theories |>
    9.41 -          (List.app (build_theories last_timing Path.current)
    9.42 +          (List.app (build_theories symbols last_timing Path.current)
    9.43              |> session_timing name verbose
    9.44              |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
    9.45              |> Multithreading.max_threads_setmp (Options.int options "threads")
    9.46 @@ -161,7 +164,6 @@
    9.47        val res2 = Exn.capture Session.finish ();
    9.48        val _ = Par_Exn.release_all [res1, res2];
    9.49  
    9.50 -      val _ = HTML.reset_symbols ();
    9.51        val _ = Options.reset_default ();
    9.52        val _ = if do_output then () else exit 0;
    9.53      in () end);
    9.54 @@ -171,15 +173,19 @@
    9.55  
    9.56  val _ =
    9.57    Isabelle_Process.protocol_command "build_theories"
    9.58 -    (fn [id, master_dir, theories_yxml] =>
    9.59 +    (fn [id, symbol_codes_yxml, master_dir, theories_yxml] =>
    9.60        let
    9.61 +        val symbols =
    9.62 +          YXML.parse_body symbol_codes_yxml
    9.63 +          |> let open XML.Decode in list (pair string int) end
    9.64 +          |> HTML.make_symbols;
    9.65          val theories =
    9.66            YXML.parse_body theories_yxml |>
    9.67              let open XML.Decode
    9.68              in list (pair Options.decode (list (string #> rpair Position.none))) end;
    9.69          val res1 =
    9.70            Exn.capture (fn () =>
    9.71 -            theories |> List.app (build_theories (K NONE) (Path.explode master_dir))) ();
    9.72 +            theories |> List.app (build_theories symbols (K NONE) (Path.explode master_dir))) ();
    9.73          val res2 = Exn.capture Session.shutdown ();
    9.74          val result =
    9.75            (Par_Exn.release_all [res1, res2]; "") handle exn =>