# HG changeset patch # User wenzelm # Date 1444411513 -7200 # Node ID 93224745477f7064ec4aa9ca3031f3a18e4f7707 # Parent 0f91067f6f73971f5abe3ae4592409ad21515168 output HTML text according to Isabelle/Scala Symbol.Interpretation; diff -r 0f91067f6f73 -r 93224745477f src/Pure/General/symbol.scala --- 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) diff -r 0f91067f6f73 -r 93224745477f src/Pure/PIDE/protocol.ML --- 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 diff -r 0f91067f6f73 -r 93224745477f src/Pure/PIDE/protocol.scala --- 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]] = diff -r 0f91067f6f73 -r 93224745477f src/Pure/PIDE/session.scala --- 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) } } } diff -r 0f91067f6f73 -r 93224745477f src/Pure/Thy/html.ML --- 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, "'")), - ("\\", (1, "¡")), - ("\\", (1, "¢")), - ("\\", (1, "£")), - ("\\", (1, "¤")), - ("\\", (1, "¥")), - ("\\", (1, "¦")), - ("\\
", (1, "§")), - ("\\", (1, "¨")), - ("\\", (1, "©")), - ("\\", (1, "ª")), - ("\\", (1, "«")), - ("\\", (1, "¬")), - ("\\", (1, "­")), - ("\\", (1, "®")), - ("\\", (1, "¯")), - ("\\", (1, "°")), - ("\\", (1, "±")), - ("\\", (1, "´")), - ("\\", (1, "¶")), - ("\\", (1, "·")), - ("\\", (1, "¸")), - ("\\", (1, "º")), - ("\\", (1, "»")), - ("\\", (1, "¼")), - ("\\", (1, "½")), - ("\\", (1, "¾")), - ("\\", (1, "¿")), - ("\\", (1, "×")), - ("\\
", (1, "÷")), - ("\\", (1, "o")), - ("\\", (1, "Α")), - ("\\", (1, "Β")), - ("\\", (1, "Γ")), - ("\\", (1, "Δ")), - ("\\", (1, "Ε")), - ("\\", (1, "Ζ")), - ("\\", (1, "Η")), - ("\\", (1, "Θ")), - ("\\", (1, "Ι")), - ("\\", (1, "Κ")), - ("\\", (1, "Λ")), - ("\\", (1, "Μ")), - ("\\", (1, "Ν")), - ("\\", (1, "Ξ")), - ("\\", (1, "Ο")), - ("\\", (1, "Π")), - ("\\", (1, "Ρ")), - ("\\", (1, "Σ")), - ("\\", (1, "Τ")), - ("\\", (1, "Υ")), - ("\\", (1, "Φ")), - ("\\", (1, "Χ")), - ("\\", (1, "Ψ")), - ("\\", (1, "Ω")), - ("\\", (1, "α")), - ("\\", (1, "β")), - ("\\", (1, "γ")), - ("\\", (1, "δ")), - ("\\", (1, "ε")), - ("\\", (1, "ζ")), - ("\\", (1, "η")), - ("\\", (1, "ϑ")), - ("\\", (1, "ι")), - ("\\", (1, "κ")), - ("\\", (1, "λ")), - ("\\", (1, "μ")), - ("\\", (1, "ν")), - ("\\", (1, "ξ")), - ("\\", (1, "ο")), - ("\\", (1, "π")), - ("\\", (1, "ρ")), - ("\\", (1, "σ")), - ("\\", (1, "τ")), - ("\\", (1, "υ")), - ("\\", (1, "φ")), - ("\\", (1, "χ")), - ("\\", (1, "ψ")), - ("\\", (1, "ω")), - ("\\", (1, "•")), - ("\\", (1, "…")), - ("\\", (1, "℘")), - ("\\", (1, "∀")), - ("\\", (1, "∂")), - ("\\", (1, "∃")), - ("\\", (1, "∅")), - ("\\", (1, "∇")), - ("\\", (1, "∈")), - ("\\", (1, "∉")), - ("\\", (1, "∏")), - ("\\", (1, "∑")), - ("\\", (1, "∗")), - ("\\", (1, "∝")), - ("\\", (1, "∞")), - ("\\", (1, "∠")), - ("\\", (1, "∧")), - ("\\", (1, "∨")), - ("\\", (1, "∩")), - ("\\", (1, "∪")), - ("\\", (1, "∼")), - ("\\", (1, "≅")), - ("\\", (1, "≈")), - ("\\", (1, "≠")), - ("\\", (1, "≡")), - ("\\", (1, "≤")), - ("\\", (1, "≥")), - ("\\", (1, "⊂")), - ("\\", (1, "⊃")), - ("\\", (1, "⊆")), - ("\\", (1, "⊇")), - ("\\", (1, "⊕")), - ("\\", (1, "⊗")), - ("\\", (1, "⊥")), - ("\\", (1, "⌈")), - ("\\", (1, "⌉")), - ("\\", (1, "⌊")), - ("\\", (1, "⌋")), - ("\\", (1, "⟨")), - ("\\", (1, "⟩")), - ("\\", (1, "◊")), - ("\\", (1, "♠")), - ("\\", (1, "♣")), - ("\\", (1, "♥")), - ("\\", (1, "♦")), - ("\\", (2, "[|")), - ("\\", (2, "|]")), - ("\\", (3, "==>")), - ("\\", (2, "=>")), - ("\\", (2, "!!")), - ("\\", (2, "::")), - ("\\", (2, "(|")), - ("\\", (2, "|)),")), - ("\\", (3, "<->")), - ("\\", (3, "-->")), - ("\\", (2, "->")), - ("\\", (1, "‹")), - ("\\", (1, "›")), - ("\\", (1, "⏎")), - ("\\<^bsub>", (0, hidden "⇘" ^ "")), - ("\\<^esub>", (0, hidden "⇙" ^ "")), - ("\\<^bsup>", (0, hidden "⇗" ^ "")), - ("\\<^esup>", (0, hidden "⇖" ^ ""))]; +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 ("", ""); +val output_sup = output_markup ("", ""); +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 "⇩" s2, ss) + else if s1 = "\\<^sup>" then (output_sup "⇧" s2, ss) + else if s1 = "\\<^bold>" then (output_bold "❙" s2, ss) + else (output_sym s1, rest); + in output_syms r (s :: result, width + w) end; - val output_sub = output_markup ("", ""); - val output_sup = output_markup ("", ""); - 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 "⇩" s2, ss) - else if s1 = "\\<^sup>" then (output_sup "⇧" s2, ss) - else if s1 = "\\<^bold>" then (output_bold "❙" 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, "'")), + ("\\<^bsub>", (0, hidden "⇘" ^ "")), + ("\\<^esub>", (0, hidden "⇙" ^ "")), + ("\\<^bsup>", (0, hidden "⇗" ^ "")), + ("\\<^esup>", (0, hidden "⇖" ^ ""))]; + in Synchronized.change symbols (K (SOME (fold Symtab.update mapping Symtab.empty))) end; + end; diff -r 0f91067f6f73 -r 93224745477f src/Pure/Tools/build.ML --- 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); diff -r 0f91067f6f73 -r 93224745477f src/Pure/Tools/build.scala --- 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 =