output HTML text according to Isabelle/Scala Symbol.Interpretation;

--- a/src/Pure/General/symbol.scala	Fri Oct 09 17:15:53 2015 +0200
+++ b/src/Pure/General/symbol.scala	Fri Oct 09 19:25:13 2015 +0200
@@ -336,29 +336,32 @@
           ("abbrev", a) <- props.reverse
         } yield sym -> a): _*)
 
+    val codes: List[(String, Int)] =
+    {
+      val Code = new Properties.String("code")
+      for {
+        (sym, props) <- symbols
+        code =
+          props match {
+            case Code(s) =>
+              try { Integer.decode(s).intValue }
+              catch { case _: NumberFormatException => error("Bad code for symbol " + sym) }
+            case _ => error("Missing code for symbol " + sym)
+          }
+      } yield {
+        if (code < 128) error("Illegal ASCII code for symbol " + sym)
+        else (sym, code)
+      }
+    }
+
 
     /* recoding */
 
-    private val Code = new Properties.String("code")
     private val (decoder, encoder) =
     {
       val mapping =
-        for {
-          (sym, props) <- symbols
-          code =
-            props match {
-              case Code(s) =>
-                try { Integer.decode(s).intValue }
-                catch { case _: NumberFormatException => error("Bad code for symbol " + sym) }
-              case _ => error("Missing code for symbol " + sym)
-            }
-          ch = new String(Character.toChars(code))
-        } yield {
-          if (code < 128) error("Illegal ASCII code for symbol " + sym)
-          else (sym, ch)
-        }
-      (new Recoder(mapping),
-       new Recoder(mapping map { case (x, y) => (y, x) }))
+        for ((sym, code) <- codes) yield (sym, new String(Character.toChars(code)))
+      (new Recoder(mapping), new Recoder(for ((x, y) <- mapping) yield (y, x)))
     }
 
     def decode(text: String): String = decoder.recode(text)
@@ -457,6 +460,7 @@
   def names: Map[Symbol, String] = symbols.names
   def groups: List[(String, List[Symbol])] = symbols.groups
   def abbrevs: Multi_Map[Symbol, String] = symbols.abbrevs
+  def codes: List[(String, Int)] = symbols.codes
 
   def decode(text: String): String = symbols.decode(text)
   def encode(text: String): String = symbols.encode(text)

--- a/src/Pure/PIDE/protocol.ML	Fri Oct 09 17:15:53 2015 +0200
+++ b/src/Pure/PIDE/protocol.ML	Fri Oct 09 19:25:13 2015 +0200
@@ -12,6 +12,13 @@
     (fn args => List.app writeln args);
 
 val _ =
+  Isabelle_Process.protocol_command "Prover.init_symbols"
+    (fn [codes_yxml] =>
+      YXML.parse_body codes_yxml
+      |> let open XML.Decode in list (pair string int) end
+      |> HTML.init_symbols);
+
+val _ =
   Isabelle_Process.protocol_command "Prover.options"
     (fn [options_yxml] =>
       let val options = Options.decode (YXML.parse_body options_yxml) in

--- a/src/Pure/PIDE/protocol.scala	Fri Oct 09 17:15:53 2015 +0200
+++ b/src/Pure/PIDE/protocol.scala	Fri Oct 09 19:25:13 2015 +0200
@@ -308,6 +308,19 @@
   def protocol_command(name: String, args: String*): Unit
 
 
+  /* symbols */
+
+  def init_symbols(): Unit =
+  {
+    val codes_yxml =
+    {
+      import XML.Encode._
+      YXML.string_of_body(list(pair(string, int))(Symbol.codes))
+    }
+    protocol_command("Prover.init_symbols", codes_yxml)
+  }
+
+
   /* options */
 
   def options(opts: Options): Unit =
@@ -322,7 +335,8 @@
   def define_command(command: Command)
   {
     val blobs_yxml =
-    { import XML.Encode._
+    {
+      import XML.Encode._
       val encode_blob: T[Command.Blob] =
         variant(List(
           { case Exn.Res((a, b)) =>
@@ -334,7 +348,8 @@
 
     val toks = command.span.content
     val toks_yxml =
-    { import XML.Encode._
+    {
+      import XML.Encode._
       val encode_tok: T[Token] =
         (tok => pair(int, int)((tok.kind.id, Symbol.iterator(tok.source).length)))
       YXML.string_of_body(list(encode_tok)(toks))
@@ -361,7 +376,8 @@
     edits: List[Document.Edit_Command])
   {
     val edits_yxml =
-    { import XML.Encode._
+    {
+      import XML.Encode._
       def id: T[Command] = (cmd => long(cmd.id))
       def encode_edit(name: Document.Node.Name)
           : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =

--- a/src/Pure/PIDE/session.scala	Fri Oct 09 17:15:53 2015 +0200
+++ b/src/Pure/PIDE/session.scala	Fri Oct 09 19:25:13 2015 +0200
@@ -494,6 +494,7 @@
               accumulate(state_id, output.message)
 
             case _ if output.is_init =>
+              prover.get.init_symbols()
               phase = Session.Ready
 
             case Markup.Return_Code(rc) if output.is_exit =>
@@ -501,7 +502,8 @@
               else phase = Session.Failed
               prover.reset
 
-            case _ => raw_output_messages.post(output)
+            case _ =>
+              raw_output_messages.post(output)
           }
         }
     }

--- a/src/Pure/Thy/html.ML	Fri Oct 09 17:15:53 2015 +0200
+++ b/src/Pure/Thy/html.ML	Fri Oct 09 19:25:13 2015 +0200
@@ -7,6 +7,8 @@
 signature HTML =
 sig
   val html_mode: ('a -> 'b) -> 'a -> 'b
+  val reset_symbols: unit -> unit
+  val init_symbols: (string * int) list -> unit
   type text = string
   val plain: string -> text
   val name: string -> text
@@ -45,179 +47,41 @@
 (* symbol output *)
 
 local
-  val hidden = span Markup.hiddenN |-> enclose;
+
+val hidden = span Markup.hiddenN |-> enclose;
+
+val symbols =
+  Synchronized.var "HTML.symbols" (NONE: (int * string) Symtab.table option);
+
+fun output_sym s =
+  if Symbol.is_raw s then (1, Symbol.decode_raw s)
+  else
+    (case Synchronized.value symbols of
+      SOME tab =>
+        (case Symtab.lookup tab s of
+          SOME x => x
+        | NONE => (size s, XML.text s))
+    | NONE => raise Fail "Missing HTML.init_symbols: cannot output symbols");
 
-  (* FIXME proper unicode -- produced on Scala side *)
-  val html_syms = Symtab.make
-   [("", (0, "")),
-    ("'", (1, "'")),
-    ("\\<exclamdown>", (1, "&iexcl;")),
-    ("\\<cent>", (1, "&cent;")),
-    ("\\<pounds>", (1, "&pound;")),
-    ("\\<currency>", (1, "&curren;")),
-    ("\\<yen>", (1, "&yen;")),
-    ("\\<bar>", (1, "&brvbar;")),
-    ("\\<section>", (1, "&sect;")),
-    ("\\<dieresis>", (1, "&uml;")),
-    ("\\<copyright>", (1, "&copy;")),
-    ("\\<ordfeminine>", (1, "&ordf;")),
-    ("\\<guillemotleft>", (1, "&laquo;")),
-    ("\\<not>", (1, "&not;")),
-    ("\\<hyphen>", (1, "&shy;")),
-    ("\\<registered>", (1, "&reg;")),
-    ("\\<inverse>", (1, "&macr;")),
-    ("\\<degree>", (1, "&deg;")),
-    ("\\<plusminus>", (1, "&plusmn;")),
-    ("\\<acute>", (1, "&acute;")),
-    ("\\<paragraph>", (1, "&para;")),
-    ("\\<cdot>", (1, "&middot;")),
-    ("\\<cedilla>", (1, "&cedil;")),
-    ("\\<ordmasculine>", (1, "&ordm;")),
-    ("\\<guillemotright>", (1, "&raquo;")),
-    ("\\<onequarter>", (1, "&frac14;")),
-    ("\\<onehalf>", (1, "&frac12;")),
-    ("\\<threequarters>", (1, "&frac34;")),
-    ("\\<questiondown>", (1, "&iquest;")),
-    ("\\<times>", (1, "&times;")),
-    ("\\<div>", (1, "&divide;")),
-    ("\\<circ>", (1, "o")),
-    ("\\<Alpha>", (1, "&Alpha;")),
-    ("\\<Beta>", (1, "&Beta;")),
-    ("\\<Gamma>", (1, "&Gamma;")),
-    ("\\<Delta>", (1, "&Delta;")),
-    ("\\<Epsilon>", (1, "&Epsilon;")),
-    ("\\<Zeta>", (1, "&Zeta;")),
-    ("\\<Eta>", (1, "&Eta;")),
-    ("\\<Theta>", (1, "&Theta;")),
-    ("\\<Iota>", (1, "&Iota;")),
-    ("\\<Kappa>", (1, "&Kappa;")),
-    ("\\<Lambda>", (1, "&Lambda;")),
-    ("\\<Mu>", (1, "&Mu;")),
-    ("\\<Nu>", (1, "&Nu;")),
-    ("\\<Xi>", (1, "&Xi;")),
-    ("\\<Omicron>", (1, "&Omicron;")),
-    ("\\<Pi>", (1, "&Pi;")),
-    ("\\<Rho>", (1, "&Rho;")),
-    ("\\<Sigma>", (1, "&Sigma;")),
-    ("\\<Tau>", (1, "&Tau;")),
-    ("\\<Upsilon>", (1, "&Upsilon;")),
-    ("\\<Phi>", (1, "&Phi;")),
-    ("\\<Chi>", (1, "&Chi;")),
-    ("\\<Psi>", (1, "&Psi;")),
-    ("\\<Omega>", (1, "&Omega;")),
-    ("\\<alpha>", (1, "&alpha;")),
-    ("\\<beta>", (1, "&beta;")),
-    ("\\<gamma>", (1, "&gamma;")),
-    ("\\<delta>", (1, "&delta;")),
-    ("\\<epsilon>", (1, "&epsilon;")),
-    ("\\<zeta>", (1, "&zeta;")),
-    ("\\<eta>", (1, "&eta;")),
-    ("\\<theta>", (1, "&thetasym;")),
-    ("\\<iota>", (1, "&iota;")),
-    ("\\<kappa>", (1, "&kappa;")),
-    ("\\<lambda>", (1, "&lambda;")),
-    ("\\<mu>", (1, "&mu;")),
-    ("\\<nu>", (1, "&nu;")),
-    ("\\<xi>", (1, "&xi;")),
-    ("\\<omicron>", (1, "&omicron;")),
-    ("\\<pi>", (1, "&pi;")),
-    ("\\<rho>", (1, "&rho;")),
-    ("\\<sigma>", (1, "&sigma;")),
-    ("\\<tau>", (1, "&tau;")),
-    ("\\<upsilon>", (1, "&upsilon;")),
-    ("\\<phi>", (1, "&phi;")),
-    ("\\<chi>", (1, "&chi;")),
-    ("\\<psi>", (1, "&psi;")),
-    ("\\<omega>", (1, "&omega;")),
-    ("\\<bullet>", (1, "&bull;")),
-    ("\\<dots>", (1, "&hellip;")),
-    ("\\<wp>", (1, "&weierp;")),
-    ("\\<forall>", (1, "&forall;")),
-    ("\\<partial>", (1, "&part;")),
-    ("\\<exists>", (1, "&exist;")),
-    ("\\<emptyset>", (1, "&empty;")),
-    ("\\<nabla>", (1, "&nabla;")),
-    ("\\<in>", (1, "&isin;")),
-    ("\\<notin>", (1, "&notin;")),
-    ("\\<Prod>", (1, "&prod;")),
-    ("\\<Sum>", (1, "&sum;")),
-    ("\\<star>", (1, "&lowast;")),
-    ("\\<propto>", (1, "&prop;")),
-    ("\\<infinity>", (1, "&infin;")),
-    ("\\<angle>", (1, "&ang;")),
-    ("\\<and>", (1, "&and;")),
-    ("\\<or>", (1, "&or;")),
-    ("\\<inter>", (1, "&cap;")),
-    ("\\<union>", (1, "&cup;")),
-    ("\\<sim>", (1, "&sim;")),
-    ("\\<cong>", (1, "&cong;")),
-    ("\\<approx>", (1, "&asymp;")),
-    ("\\<noteq>", (1, "&ne;")),
-    ("\\<equiv>", (1, "&equiv;")),
-    ("\\<le>", (1, "&le;")),
-    ("\\<ge>", (1, "&ge;")),
-    ("\\<subset>", (1, "&sub;")),
-    ("\\<supset>", (1, "&sup;")),
-    ("\\<subseteq>", (1, "&sube;")),
-    ("\\<supseteq>", (1, "&supe;")),
-    ("\\<oplus>", (1, "&oplus;")),
-    ("\\<otimes>", (1, "&otimes;")),
-    ("\\<bottom>", (1, "&perp;")),
-    ("\\<lceil>", (1, "&lceil;")),
-    ("\\<rceil>", (1, "&rceil;")),
-    ("\\<lfloor>", (1, "&lfloor;")),
-    ("\\<rfloor>", (1, "&rfloor;")),
-    ("\\<langle>", (1, "&lang;")),
-    ("\\<rangle>", (1, "&rang;")),
-    ("\\<lozenge>", (1, "&loz;")),
-    ("\\<spadesuit>", (1, "&spades;")),
-    ("\\<clubsuit>", (1, "&clubs;")),
-    ("\\<heartsuit>", (1, "&hearts;")),
-    ("\\<diamondsuit>", (1, "&diams;")),
-    ("\\<lbrakk>", (2, "[|")),
-    ("\\<rbrakk>", (2, "|]")),
-    ("\\<Longrightarrow>", (3, "==&gt;")),
-    ("\\<Rightarrow>", (2, "=&gt;")),
-    ("\\<And>", (2, "!!")),
-    ("\\<Colon>", (2, "::")),
-    ("\\<lparr>", (2, "(|")),
-    ("\\<rparr>", (2, "|)),")),
-    ("\\<longleftrightarrow>", (3, "&lt;-&gt;")),
-    ("\\<longrightarrow>", (3, "--&gt;")),
-    ("\\<rightarrow>", (2, "-&gt;")),
-    ("\\<open>", (1, "&#8249;")),
-    ("\\<close>", (1, "&#8250;")),
-    ("\\<newline>", (1, "&#9166;")),
-    ("\\<^bsub>", (0, hidden "&#8664;" ^ "<sub>")),
-    ("\\<^esub>", (0, hidden "&#8665;" ^ "</sub>")),
-    ("\\<^bsup>", (0, hidden "&#8663;" ^ "<sup>")),
-    ("\\<^esup>", (0, hidden "&#8662;" ^ "</sup>"))];
+fun output_markup (bg, en) s1 s2 =
+  let val (n, txt) = output_sym s2
+  in (n, hidden s1 ^ enclose bg en txt) end;
+
+val output_sub = output_markup ("<sub>", "</sub>");
+val output_sup = output_markup ("<sup>", "</sup>");
+val output_bold = output_markup (span "bold");
 
-  fun output_sym s =
-    if Symbol.is_raw s then (1, Symbol.decode_raw s)
-    else
-      (case Symtab.lookup html_syms s of
-        SOME x => x
-      | NONE => (size s, XML.text s));
-
-  fun output_markup (bg, en) s1 s2 =
-    let val (n, txt) = output_sym s2
-    in (n, hidden s1 ^ enclose bg en txt) end;
+fun output_syms [] (result, width) = (implode (rev result), width)
+  | output_syms (s1 :: rest) (result, width) =
+      let
+        val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss));
+        val ((w, s), r) =
+          if s1 = "\\<^sub>" then (output_sub "&#8681;" s2, ss)
+          else if s1 = "\\<^sup>" then (output_sup "&#8679;" s2, ss)
+          else if s1 = "\\<^bold>" then (output_bold "&#10073;" s2, ss)
+          else (output_sym s1, rest);
+      in output_syms r (s :: result, width + w) end;
 
-  val output_sub = output_markup ("<sub>", "</sub>");
-  val output_sup = output_markup ("<sup>", "</sup>");
-  val output_bold = output_markup (span "bold");
-
-  fun output_syms [] (result, width) = (implode (rev result), width)
-    | output_syms (s1 :: rest) (result, width) =
-        let
-          val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss));
-          val ((w, s), r) =
-            if s1 = "\\<^sub>" then (output_sub "&#8681;" s2, ss)
-            else if s1 = "\\<^sup>" then (output_sup "&#8679;" s2, ss)
-            else if s1 = "\\<^bold>" then (output_bold "&#10073;" s2, ss)
-            else (output_sym s1, rest);
-        in output_syms r (s :: result, width + w) end;
 in
 
 fun output_width str = output_syms (Symbol.explode str) ([], 0);
@@ -225,6 +89,21 @@
 
 val _ = Output.add_mode htmlN output_width Symbol.encode_raw;
 
+
+fun reset_symbols () = Synchronized.change symbols (K NONE);
+
+fun init_symbols codes =
+  let
+    val mapping =
+      map (fn (s, c) => (s, (Symbol.length [s], "&#" ^ Markup.print_int c ^ ";"))) codes @
+       [("", (0, "")),
+        ("'", (1, "&#39;")),
+        ("\\<^bsub>", (0, hidden "&#8664;" ^ "<sub>")),
+        ("\\<^esub>", (0, hidden "&#8665;" ^ "</sub>")),
+        ("\\<^bsup>", (0, hidden "&#8663;" ^ "<sup>")),
+        ("\\<^esup>", (0, hidden "&#8662;" ^ "</sup>"))];
+  in Synchronized.change symbols (K (SOME (fold Symtab.update mapping Symtab.empty))) end;
+
 end;
 
 

--- a/src/Pure/Tools/build.ML	Fri Oct 09 17:15:53 2015 +0200
+++ b/src/Pure/Tools/build.ML	Fri Oct 09 19:25:13 2015 +0200
@@ -123,15 +123,17 @@
     let
       val _ = SHA1_Samples.test ();
 
-      val (command_timings, (do_output, (options, (verbose, (browser_info,
-          (document_files, (graph_file, (parent_name, (chapter, (name, theories)))))))))) =
+      val (symbol_codes, (command_timings, (do_output, (options, (verbose, (browser_info,
+          (document_files, (graph_file, (parent_name, (chapter, (name, theories))))))))))) =
         File.read (Path.explode args_file) |> YXML.parse_body |>
           let open XML.Decode in
-            pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
-              (pair (list (pair string string)) (pair string (pair string (pair string (pair string
-                ((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))
+            pair (list (pair string int)) (pair (list properties) (pair bool (pair Options.decode
+              (pair bool (pair string (pair (list (pair string string)) (pair string
+                (pair string (pair string (pair string
+                ((list (pair Options.decode (list (string #> rpair Position.none)))))))))))))))
           end;
 
+      val _ = HTML.init_symbols symbol_codes;
       val _ = Options.set_default options;
 
       val _ = writeln ("\fSession.name = " ^ name);
@@ -159,6 +161,7 @@
       val res2 = Exn.capture Session.finish ();
       val _ = Par_Exn.release_all [res1, res2];
 
+      val _ = HTML.reset_symbols ();
       val _ = Options.reset_default ();
       val _ = if do_output then () else exit 0;
     in () end);

--- a/src/Pure/Tools/build.scala	Fri Oct 09 17:15:53 2015 +0200
+++ b/src/Pure/Tools/build.scala	Fri Oct 09 19:25:13 2015 +0200
@@ -553,12 +553,14 @@
         {
           val theories = info.theories.map(x => (x._2, x._3))
           import XML.Encode._
-              pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
-                pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string,
-                pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))))(
-              (command_timings, (do_output, (info.options, (verbose, (browser_info,
-                (info.document_files, (File.standard_path(graph_file), (parent,
-                (info.chapter, (name, theories)))))))))))
+          pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(Options.encode,
+            pair(bool, pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
+            pair(string, pair(string, pair(string,
+            list(pair(Options.encode, list(Path.encode))))))))))))))(
+          (Symbol.codes, (command_timings, (do_output, (info.options,
+            (verbose, (browser_info, (info.document_files, (File.standard_path(graph_file),
+            (parent, (info.chapter, (name,
+            theories))))))))))))
         }))
 
     private val env =