output HTML text according to Isabelle/Scala Symbol.Interpretation;
authorwenzelm
Fri Oct 09 19:25:13 2015 +0200 (2015-10-09)
changeset 6137693224745477f
parent 61375 0f91067f6f73
child 61377 517feb558c77
output HTML text according to Isabelle/Scala Symbol.Interpretation;
src/Pure/General/symbol.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/session.scala
src/Pure/Thy/html.ML
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/General/symbol.scala	Fri Oct 09 17:15:53 2015 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Fri Oct 09 19:25:13 2015 +0200
     1.3 @@ -336,29 +336,32 @@
     1.4            ("abbrev", a) <- props.reverse
     1.5          } yield sym -> a): _*)
     1.6  
     1.7 +    val codes: List[(String, Int)] =
     1.8 +    {
     1.9 +      val Code = new Properties.String("code")
    1.10 +      for {
    1.11 +        (sym, props) <- symbols
    1.12 +        code =
    1.13 +          props match {
    1.14 +            case Code(s) =>
    1.15 +              try { Integer.decode(s).intValue }
    1.16 +              catch { case _: NumberFormatException => error("Bad code for symbol " + sym) }
    1.17 +            case _ => error("Missing code for symbol " + sym)
    1.18 +          }
    1.19 +      } yield {
    1.20 +        if (code < 128) error("Illegal ASCII code for symbol " + sym)
    1.21 +        else (sym, code)
    1.22 +      }
    1.23 +    }
    1.24 +
    1.25  
    1.26      /* recoding */
    1.27  
    1.28 -    private val Code = new Properties.String("code")
    1.29      private val (decoder, encoder) =
    1.30      {
    1.31        val mapping =
    1.32 -        for {
    1.33 -          (sym, props) <- symbols
    1.34 -          code =
    1.35 -            props match {
    1.36 -              case Code(s) =>
    1.37 -                try { Integer.decode(s).intValue }
    1.38 -                catch { case _: NumberFormatException => error("Bad code for symbol " + sym) }
    1.39 -              case _ => error("Missing code for symbol " + sym)
    1.40 -            }
    1.41 -          ch = new String(Character.toChars(code))
    1.42 -        } yield {
    1.43 -          if (code < 128) error("Illegal ASCII code for symbol " + sym)
    1.44 -          else (sym, ch)
    1.45 -        }
    1.46 -      (new Recoder(mapping),
    1.47 -       new Recoder(mapping map { case (x, y) => (y, x) }))
    1.48 +        for ((sym, code) <- codes) yield (sym, new String(Character.toChars(code)))
    1.49 +      (new Recoder(mapping), new Recoder(for ((x, y) <- mapping) yield (y, x)))
    1.50      }
    1.51  
    1.52      def decode(text: String): String = decoder.recode(text)
    1.53 @@ -457,6 +460,7 @@
    1.54    def names: Map[Symbol, String] = symbols.names
    1.55    def groups: List[(String, List[Symbol])] = symbols.groups
    1.56    def abbrevs: Multi_Map[Symbol, String] = symbols.abbrevs
    1.57 +  def codes: List[(String, Int)] = symbols.codes
    1.58  
    1.59    def decode(text: String): String = symbols.decode(text)
    1.60    def encode(text: String): String = symbols.encode(text)
     2.1 --- a/src/Pure/PIDE/protocol.ML	Fri Oct 09 17:15:53 2015 +0200
     2.2 +++ b/src/Pure/PIDE/protocol.ML	Fri Oct 09 19:25:13 2015 +0200
     2.3 @@ -12,6 +12,13 @@
     2.4      (fn args => List.app writeln args);
     2.5  
     2.6  val _ =
     2.7 +  Isabelle_Process.protocol_command "Prover.init_symbols"
     2.8 +    (fn [codes_yxml] =>
     2.9 +      YXML.parse_body codes_yxml
    2.10 +      |> let open XML.Decode in list (pair string int) end
    2.11 +      |> HTML.init_symbols);
    2.12 +
    2.13 +val _ =
    2.14    Isabelle_Process.protocol_command "Prover.options"
    2.15      (fn [options_yxml] =>
    2.16        let val options = Options.decode (YXML.parse_body options_yxml) in
     3.1 --- a/src/Pure/PIDE/protocol.scala	Fri Oct 09 17:15:53 2015 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Oct 09 19:25:13 2015 +0200
     3.3 @@ -308,6 +308,19 @@
     3.4    def protocol_command(name: String, args: String*): Unit
     3.5  
     3.6  
     3.7 +  /* symbols */
     3.8 +
     3.9 +  def init_symbols(): Unit =
    3.10 +  {
    3.11 +    val codes_yxml =
    3.12 +    {
    3.13 +      import XML.Encode._
    3.14 +      YXML.string_of_body(list(pair(string, int))(Symbol.codes))
    3.15 +    }
    3.16 +    protocol_command("Prover.init_symbols", codes_yxml)
    3.17 +  }
    3.18 +
    3.19 +
    3.20    /* options */
    3.21  
    3.22    def options(opts: Options): Unit =
    3.23 @@ -322,7 +335,8 @@
    3.24    def define_command(command: Command)
    3.25    {
    3.26      val blobs_yxml =
    3.27 -    { import XML.Encode._
    3.28 +    {
    3.29 +      import XML.Encode._
    3.30        val encode_blob: T[Command.Blob] =
    3.31          variant(List(
    3.32            { case Exn.Res((a, b)) =>
    3.33 @@ -334,7 +348,8 @@
    3.34  
    3.35      val toks = command.span.content
    3.36      val toks_yxml =
    3.37 -    { import XML.Encode._
    3.38 +    {
    3.39 +      import XML.Encode._
    3.40        val encode_tok: T[Token] =
    3.41          (tok => pair(int, int)((tok.kind.id, Symbol.iterator(tok.source).length)))
    3.42        YXML.string_of_body(list(encode_tok)(toks))
    3.43 @@ -361,7 +376,8 @@
    3.44      edits: List[Document.Edit_Command])
    3.45    {
    3.46      val edits_yxml =
    3.47 -    { import XML.Encode._
    3.48 +    {
    3.49 +      import XML.Encode._
    3.50        def id: T[Command] = (cmd => long(cmd.id))
    3.51        def encode_edit(name: Document.Node.Name)
    3.52            : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
     4.1 --- a/src/Pure/PIDE/session.scala	Fri Oct 09 17:15:53 2015 +0200
     4.2 +++ b/src/Pure/PIDE/session.scala	Fri Oct 09 19:25:13 2015 +0200
     4.3 @@ -494,6 +494,7 @@
     4.4                accumulate(state_id, output.message)
     4.5  
     4.6              case _ if output.is_init =>
     4.7 +              prover.get.init_symbols()
     4.8                phase = Session.Ready
     4.9  
    4.10              case Markup.Return_Code(rc) if output.is_exit =>
    4.11 @@ -501,7 +502,8 @@
    4.12                else phase = Session.Failed
    4.13                prover.reset
    4.14  
    4.15 -            case _ => raw_output_messages.post(output)
    4.16 +            case _ =>
    4.17 +              raw_output_messages.post(output)
    4.18            }
    4.19          }
    4.20      }
     5.1 --- a/src/Pure/Thy/html.ML	Fri Oct 09 17:15:53 2015 +0200
     5.2 +++ b/src/Pure/Thy/html.ML	Fri Oct 09 19:25:13 2015 +0200
     5.3 @@ -7,6 +7,8 @@
     5.4  signature HTML =
     5.5  sig
     5.6    val html_mode: ('a -> 'b) -> 'a -> 'b
     5.7 +  val reset_symbols: unit -> unit
     5.8 +  val init_symbols: (string * int) list -> unit
     5.9    type text = string
    5.10    val plain: string -> text
    5.11    val name: string -> text
    5.12 @@ -45,179 +47,41 @@
    5.13  (* symbol output *)
    5.14  
    5.15  local
    5.16 -  val hidden = span Markup.hiddenN |-> enclose;
    5.17 +
    5.18 +val hidden = span Markup.hiddenN |-> enclose;
    5.19 +
    5.20 +val symbols =
    5.21 +  Synchronized.var "HTML.symbols" (NONE: (int * string) Symtab.table option);
    5.22 +
    5.23 +fun output_sym s =
    5.24 +  if Symbol.is_raw s then (1, Symbol.decode_raw s)
    5.25 +  else
    5.26 +    (case Synchronized.value symbols of
    5.27 +      SOME tab =>
    5.28 +        (case Symtab.lookup tab s of
    5.29 +          SOME x => x
    5.30 +        | NONE => (size s, XML.text s))
    5.31 +    | NONE => raise Fail "Missing HTML.init_symbols: cannot output symbols");
    5.32  
    5.33 -  (* FIXME proper unicode -- produced on Scala side *)
    5.34 -  val html_syms = Symtab.make
    5.35 -   [("", (0, "")),
    5.36 -    ("'", (1, "&#39;")),
    5.37 -    ("\\<exclamdown>", (1, "&iexcl;")),
    5.38 -    ("\\<cent>", (1, "&cent;")),
    5.39 -    ("\\<pounds>", (1, "&pound;")),
    5.40 -    ("\\<currency>", (1, "&curren;")),
    5.41 -    ("\\<yen>", (1, "&yen;")),
    5.42 -    ("\\<bar>", (1, "&brvbar;")),
    5.43 -    ("\\<section>", (1, "&sect;")),
    5.44 -    ("\\<dieresis>", (1, "&uml;")),
    5.45 -    ("\\<copyright>", (1, "&copy;")),
    5.46 -    ("\\<ordfeminine>", (1, "&ordf;")),
    5.47 -    ("\\<guillemotleft>", (1, "&laquo;")),
    5.48 -    ("\\<not>", (1, "&not;")),
    5.49 -    ("\\<hyphen>", (1, "&shy;")),
    5.50 -    ("\\<registered>", (1, "&reg;")),
    5.51 -    ("\\<inverse>", (1, "&macr;")),
    5.52 -    ("\\<degree>", (1, "&deg;")),
    5.53 -    ("\\<plusminus>", (1, "&plusmn;")),
    5.54 -    ("\\<acute>", (1, "&acute;")),
    5.55 -    ("\\<paragraph>", (1, "&para;")),
    5.56 -    ("\\<cdot>", (1, "&middot;")),
    5.57 -    ("\\<cedilla>", (1, "&cedil;")),
    5.58 -    ("\\<ordmasculine>", (1, "&ordm;")),
    5.59 -    ("\\<guillemotright>", (1, "&raquo;")),
    5.60 -    ("\\<onequarter>", (1, "&frac14;")),
    5.61 -    ("\\<onehalf>", (1, "&frac12;")),
    5.62 -    ("\\<threequarters>", (1, "&frac34;")),
    5.63 -    ("\\<questiondown>", (1, "&iquest;")),
    5.64 -    ("\\<times>", (1, "&times;")),
    5.65 -    ("\\<div>", (1, "&divide;")),
    5.66 -    ("\\<circ>", (1, "o")),
    5.67 -    ("\\<Alpha>", (1, "&Alpha;")),
    5.68 -    ("\\<Beta>", (1, "&Beta;")),
    5.69 -    ("\\<Gamma>", (1, "&Gamma;")),
    5.70 -    ("\\<Delta>", (1, "&Delta;")),
    5.71 -    ("\\<Epsilon>", (1, "&Epsilon;")),
    5.72 -    ("\\<Zeta>", (1, "&Zeta;")),
    5.73 -    ("\\<Eta>", (1, "&Eta;")),
    5.74 -    ("\\<Theta>", (1, "&Theta;")),
    5.75 -    ("\\<Iota>", (1, "&Iota;")),
    5.76 -    ("\\<Kappa>", (1, "&Kappa;")),
    5.77 -    ("\\<Lambda>", (1, "&Lambda;")),
    5.78 -    ("\\<Mu>", (1, "&Mu;")),
    5.79 -    ("\\<Nu>", (1, "&Nu;")),
    5.80 -    ("\\<Xi>", (1, "&Xi;")),
    5.81 -    ("\\<Omicron>", (1, "&Omicron;")),
    5.82 -    ("\\<Pi>", (1, "&Pi;")),
    5.83 -    ("\\<Rho>", (1, "&Rho;")),
    5.84 -    ("\\<Sigma>", (1, "&Sigma;")),
    5.85 -    ("\\<Tau>", (1, "&Tau;")),
    5.86 -    ("\\<Upsilon>", (1, "&Upsilon;")),
    5.87 -    ("\\<Phi>", (1, "&Phi;")),
    5.88 -    ("\\<Chi>", (1, "&Chi;")),
    5.89 -    ("\\<Psi>", (1, "&Psi;")),
    5.90 -    ("\\<Omega>", (1, "&Omega;")),
    5.91 -    ("\\<alpha>", (1, "&alpha;")),
    5.92 -    ("\\<beta>", (1, "&beta;")),
    5.93 -    ("\\<gamma>", (1, "&gamma;")),
    5.94 -    ("\\<delta>", (1, "&delta;")),
    5.95 -    ("\\<epsilon>", (1, "&epsilon;")),
    5.96 -    ("\\<zeta>", (1, "&zeta;")),
    5.97 -    ("\\<eta>", (1, "&eta;")),
    5.98 -    ("\\<theta>", (1, "&thetasym;")),
    5.99 -    ("\\<iota>", (1, "&iota;")),
   5.100 -    ("\\<kappa>", (1, "&kappa;")),
   5.101 -    ("\\<lambda>", (1, "&lambda;")),
   5.102 -    ("\\<mu>", (1, "&mu;")),
   5.103 -    ("\\<nu>", (1, "&nu;")),
   5.104 -    ("\\<xi>", (1, "&xi;")),
   5.105 -    ("\\<omicron>", (1, "&omicron;")),
   5.106 -    ("\\<pi>", (1, "&pi;")),
   5.107 -    ("\\<rho>", (1, "&rho;")),
   5.108 -    ("\\<sigma>", (1, "&sigma;")),
   5.109 -    ("\\<tau>", (1, "&tau;")),
   5.110 -    ("\\<upsilon>", (1, "&upsilon;")),
   5.111 -    ("\\<phi>", (1, "&phi;")),
   5.112 -    ("\\<chi>", (1, "&chi;")),
   5.113 -    ("\\<psi>", (1, "&psi;")),
   5.114 -    ("\\<omega>", (1, "&omega;")),
   5.115 -    ("\\<bullet>", (1, "&bull;")),
   5.116 -    ("\\<dots>", (1, "&hellip;")),
   5.117 -    ("\\<wp>", (1, "&weierp;")),
   5.118 -    ("\\<forall>", (1, "&forall;")),
   5.119 -    ("\\<partial>", (1, "&part;")),
   5.120 -    ("\\<exists>", (1, "&exist;")),
   5.121 -    ("\\<emptyset>", (1, "&empty;")),
   5.122 -    ("\\<nabla>", (1, "&nabla;")),
   5.123 -    ("\\<in>", (1, "&isin;")),
   5.124 -    ("\\<notin>", (1, "&notin;")),
   5.125 -    ("\\<Prod>", (1, "&prod;")),
   5.126 -    ("\\<Sum>", (1, "&sum;")),
   5.127 -    ("\\<star>", (1, "&lowast;")),
   5.128 -    ("\\<propto>", (1, "&prop;")),
   5.129 -    ("\\<infinity>", (1, "&infin;")),
   5.130 -    ("\\<angle>", (1, "&ang;")),
   5.131 -    ("\\<and>", (1, "&and;")),
   5.132 -    ("\\<or>", (1, "&or;")),
   5.133 -    ("\\<inter>", (1, "&cap;")),
   5.134 -    ("\\<union>", (1, "&cup;")),
   5.135 -    ("\\<sim>", (1, "&sim;")),
   5.136 -    ("\\<cong>", (1, "&cong;")),
   5.137 -    ("\\<approx>", (1, "&asymp;")),
   5.138 -    ("\\<noteq>", (1, "&ne;")),
   5.139 -    ("\\<equiv>", (1, "&equiv;")),
   5.140 -    ("\\<le>", (1, "&le;")),
   5.141 -    ("\\<ge>", (1, "&ge;")),
   5.142 -    ("\\<subset>", (1, "&sub;")),
   5.143 -    ("\\<supset>", (1, "&sup;")),
   5.144 -    ("\\<subseteq>", (1, "&sube;")),
   5.145 -    ("\\<supseteq>", (1, "&supe;")),
   5.146 -    ("\\<oplus>", (1, "&oplus;")),
   5.147 -    ("\\<otimes>", (1, "&otimes;")),
   5.148 -    ("\\<bottom>", (1, "&perp;")),
   5.149 -    ("\\<lceil>", (1, "&lceil;")),
   5.150 -    ("\\<rceil>", (1, "&rceil;")),
   5.151 -    ("\\<lfloor>", (1, "&lfloor;")),
   5.152 -    ("\\<rfloor>", (1, "&rfloor;")),
   5.153 -    ("\\<langle>", (1, "&lang;")),
   5.154 -    ("\\<rangle>", (1, "&rang;")),
   5.155 -    ("\\<lozenge>", (1, "&loz;")),
   5.156 -    ("\\<spadesuit>", (1, "&spades;")),
   5.157 -    ("\\<clubsuit>", (1, "&clubs;")),
   5.158 -    ("\\<heartsuit>", (1, "&hearts;")),
   5.159 -    ("\\<diamondsuit>", (1, "&diams;")),
   5.160 -    ("\\<lbrakk>", (2, "[|")),
   5.161 -    ("\\<rbrakk>", (2, "|]")),
   5.162 -    ("\\<Longrightarrow>", (3, "==&gt;")),
   5.163 -    ("\\<Rightarrow>", (2, "=&gt;")),
   5.164 -    ("\\<And>", (2, "!!")),
   5.165 -    ("\\<Colon>", (2, "::")),
   5.166 -    ("\\<lparr>", (2, "(|")),
   5.167 -    ("\\<rparr>", (2, "|)),")),
   5.168 -    ("\\<longleftrightarrow>", (3, "&lt;-&gt;")),
   5.169 -    ("\\<longrightarrow>", (3, "--&gt;")),
   5.170 -    ("\\<rightarrow>", (2, "-&gt;")),
   5.171 -    ("\\<open>", (1, "&#8249;")),
   5.172 -    ("\\<close>", (1, "&#8250;")),
   5.173 -    ("\\<newline>", (1, "&#9166;")),
   5.174 -    ("\\<^bsub>", (0, hidden "&#8664;" ^ "<sub>")),
   5.175 -    ("\\<^esub>", (0, hidden "&#8665;" ^ "</sub>")),
   5.176 -    ("\\<^bsup>", (0, hidden "&#8663;" ^ "<sup>")),
   5.177 -    ("\\<^esup>", (0, hidden "&#8662;" ^ "</sup>"))];
   5.178 +fun output_markup (bg, en) s1 s2 =
   5.179 +  let val (n, txt) = output_sym s2
   5.180 +  in (n, hidden s1 ^ enclose bg en txt) end;
   5.181 +
   5.182 +val output_sub = output_markup ("<sub>", "</sub>");
   5.183 +val output_sup = output_markup ("<sup>", "</sup>");
   5.184 +val output_bold = output_markup (span "bold");
   5.185  
   5.186 -  fun output_sym s =
   5.187 -    if Symbol.is_raw s then (1, Symbol.decode_raw s)
   5.188 -    else
   5.189 -      (case Symtab.lookup html_syms s of
   5.190 -        SOME x => x
   5.191 -      | NONE => (size s, XML.text s));
   5.192 -
   5.193 -  fun output_markup (bg, en) s1 s2 =
   5.194 -    let val (n, txt) = output_sym s2
   5.195 -    in (n, hidden s1 ^ enclose bg en txt) end;
   5.196 +fun output_syms [] (result, width) = (implode (rev result), width)
   5.197 +  | output_syms (s1 :: rest) (result, width) =
   5.198 +      let
   5.199 +        val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss));
   5.200 +        val ((w, s), r) =
   5.201 +          if s1 = "\\<^sub>" then (output_sub "&#8681;" s2, ss)
   5.202 +          else if s1 = "\\<^sup>" then (output_sup "&#8679;" s2, ss)
   5.203 +          else if s1 = "\\<^bold>" then (output_bold "&#10073;" s2, ss)
   5.204 +          else (output_sym s1, rest);
   5.205 +      in output_syms r (s :: result, width + w) end;
   5.206  
   5.207 -  val output_sub = output_markup ("<sub>", "</sub>");
   5.208 -  val output_sup = output_markup ("<sup>", "</sup>");
   5.209 -  val output_bold = output_markup (span "bold");
   5.210 -
   5.211 -  fun output_syms [] (result, width) = (implode (rev result), width)
   5.212 -    | output_syms (s1 :: rest) (result, width) =
   5.213 -        let
   5.214 -          val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss));
   5.215 -          val ((w, s), r) =
   5.216 -            if s1 = "\\<^sub>" then (output_sub "&#8681;" s2, ss)
   5.217 -            else if s1 = "\\<^sup>" then (output_sup "&#8679;" s2, ss)
   5.218 -            else if s1 = "\\<^bold>" then (output_bold "&#10073;" s2, ss)
   5.219 -            else (output_sym s1, rest);
   5.220 -        in output_syms r (s :: result, width + w) end;
   5.221  in
   5.222  
   5.223  fun output_width str = output_syms (Symbol.explode str) ([], 0);
   5.224 @@ -225,6 +89,21 @@
   5.225  
   5.226  val _ = Output.add_mode htmlN output_width Symbol.encode_raw;
   5.227  
   5.228 +
   5.229 +fun reset_symbols () = Synchronized.change symbols (K NONE);
   5.230 +
   5.231 +fun init_symbols codes =
   5.232 +  let
   5.233 +    val mapping =
   5.234 +      map (fn (s, c) => (s, (Symbol.length [s], "&#" ^ Markup.print_int c ^ ";"))) codes @
   5.235 +       [("", (0, "")),
   5.236 +        ("'", (1, "&#39;")),
   5.237 +        ("\\<^bsub>", (0, hidden "&#8664;" ^ "<sub>")),
   5.238 +        ("\\<^esub>", (0, hidden "&#8665;" ^ "</sub>")),
   5.239 +        ("\\<^bsup>", (0, hidden "&#8663;" ^ "<sup>")),
   5.240 +        ("\\<^esup>", (0, hidden "&#8662;" ^ "</sup>"))];
   5.241 +  in Synchronized.change symbols (K (SOME (fold Symtab.update mapping Symtab.empty))) end;
   5.242 +
   5.243  end;
   5.244  
   5.245  
     6.1 --- a/src/Pure/Tools/build.ML	Fri Oct 09 17:15:53 2015 +0200
     6.2 +++ b/src/Pure/Tools/build.ML	Fri Oct 09 19:25:13 2015 +0200
     6.3 @@ -123,15 +123,17 @@
     6.4      let
     6.5        val _ = SHA1_Samples.test ();
     6.6  
     6.7 -      val (command_timings, (do_output, (options, (verbose, (browser_info,
     6.8 -          (document_files, (graph_file, (parent_name, (chapter, (name, theories)))))))))) =
     6.9 +      val (symbol_codes, (command_timings, (do_output, (options, (verbose, (browser_info,
    6.10 +          (document_files, (graph_file, (parent_name, (chapter, (name, theories))))))))))) =
    6.11          File.read (Path.explode args_file) |> YXML.parse_body |>
    6.12            let open XML.Decode in
    6.13 -            pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
    6.14 -              (pair (list (pair string string)) (pair string (pair string (pair string (pair string
    6.15 -                ((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))
    6.16 +            pair (list (pair string int)) (pair (list properties) (pair bool (pair Options.decode
    6.17 +              (pair bool (pair string (pair (list (pair string string)) (pair string
    6.18 +                (pair string (pair string (pair string
    6.19 +                ((list (pair Options.decode (list (string #> rpair Position.none)))))))))))))))
    6.20            end;
    6.21  
    6.22 +      val _ = HTML.init_symbols symbol_codes;
    6.23        val _ = Options.set_default options;
    6.24  
    6.25        val _ = writeln ("\fSession.name = " ^ name);
    6.26 @@ -159,6 +161,7 @@
    6.27        val res2 = Exn.capture Session.finish ();
    6.28        val _ = Par_Exn.release_all [res1, res2];
    6.29  
    6.30 +      val _ = HTML.reset_symbols ();
    6.31        val _ = Options.reset_default ();
    6.32        val _ = if do_output then () else exit 0;
    6.33      in () end);
     7.1 --- a/src/Pure/Tools/build.scala	Fri Oct 09 17:15:53 2015 +0200
     7.2 +++ b/src/Pure/Tools/build.scala	Fri Oct 09 19:25:13 2015 +0200
     7.3 @@ -553,12 +553,14 @@
     7.4          {
     7.5            val theories = info.theories.map(x => (x._2, x._3))
     7.6            import XML.Encode._
     7.7 -              pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
     7.8 -                pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string,
     7.9 -                pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))))(
    7.10 -              (command_timings, (do_output, (info.options, (verbose, (browser_info,
    7.11 -                (info.document_files, (File.standard_path(graph_file), (parent,
    7.12 -                (info.chapter, (name, theories)))))))))))
    7.13 +          pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(Options.encode,
    7.14 +            pair(bool, pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
    7.15 +            pair(string, pair(string, pair(string,
    7.16 +            list(pair(Options.encode, list(Path.encode))))))))))))))(
    7.17 +          (Symbol.codes, (command_timings, (do_output, (info.options,
    7.18 +            (verbose, (browser_info, (info.document_files, (File.standard_path(graph_file),
    7.19 +            (parent, (info.chapter, (name,
    7.20 +            theories))))))))))))
    7.21          }))
    7.22  
    7.23      private val env =