# HG changeset patch # User wenzelm # Date 1444486894 -7200 # Node ID ddca85598c659453611448b647abde93fe767713 # Parent 3907f20bef8cf97c893d9c832690c4714cf0029d more explicit HTML.symbols; tuned signature; diff -r 3907f20bef8c -r ddca85598c65 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Fri Oct 09 21:20:43 2015 +0200 +++ b/src/Pure/PIDE/protocol.ML Sat Oct 10 16:21:34 2015 +0200 @@ -12,13 +12,6 @@ (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 3907f20bef8c -r ddca85598c65 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Fri Oct 09 21:20:43 2015 +0200 +++ b/src/Pure/PIDE/protocol.scala Sat Oct 10 16:21:34 2015 +0200 @@ -308,19 +308,6 @@ 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 = @@ -425,6 +412,9 @@ def build_theories(id: String, master_dir: Path, theories: List[(Options, List[Path])]) { + val symbol_codes_yxml = + { import XML.Encode._ + YXML.string_of_body(list(pair(string, int))(Symbol.codes)) } val theories_yxml = { import XML.Encode._ YXML.string_of_body(list(pair(Options.encode, list(Path.encode)))(theories)) } diff -r 3907f20bef8c -r ddca85598c65 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Fri Oct 09 21:20:43 2015 +0200 +++ b/src/Pure/PIDE/resources.ML Sat Oct 10 16:21:34 2015 +0200 @@ -17,8 +17,9 @@ val provide_parse_files: string -> (theory -> Token.file list * theory) parser val loaded_files_current: theory -> bool val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory - val load_thy: bool -> (Toplevel.transition -> Time.time option) -> int -> Path.T -> - Thy_Header.header -> Position.T -> string -> theory list -> theory * (unit -> unit) * int + val load_thy: bool -> HTML.symbols -> (Toplevel.transition -> Time.time option) -> int -> + Path.T -> Thy_Header.header -> Position.T -> string -> theory list -> + theory * (unit -> unit) * int end; structure Resources: RESOURCES = @@ -145,7 +146,7 @@ val thy = Toplevel.end_theory end_pos end_state; in (results, thy) end; -fun load_thy document last_timing update_time master_dir header text_pos text parents = +fun load_thy document symbols last_timing update_time master_dir header text_pos text parents = let val (name, _) = #name header; val keywords = @@ -159,7 +160,7 @@ fun init () = begin_theory master_dir header parents |> Present.begin_theory update_time - (fn () => implode (map (HTML.present_span keywords) spans)); + (fn () => implode (map (HTML.present_span symbols keywords) spans)); val (results, thy) = cond_timeit true ("theory " ^ quote name) diff -r 3907f20bef8c -r ddca85598c65 src/Pure/PIDE/session.ML --- a/src/Pure/PIDE/session.ML Fri Oct 09 21:20:43 2015 +0200 +++ b/src/Pure/PIDE/session.ML Sat Oct 10 16:21:34 2015 +0200 @@ -9,7 +9,7 @@ val get_name: unit -> string val welcome: unit -> string val get_keywords: unit -> Keyword.keywords - val init: bool -> bool -> Path.T -> string -> string -> (string * string) list -> + val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list -> (Path.T * Path.T) list -> Path.T -> string -> string * string -> bool -> unit val shutdown: unit -> unit val finish: unit -> unit @@ -44,7 +44,7 @@ (* init *) -fun init build info info_path doc doc_output doc_variants doc_files graph_file +fun init symbols build info info_path doc doc_output doc_variants doc_files graph_file parent (chapter, name) verbose = if get_name () <> parent orelse not (! session_finished) then error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) @@ -53,7 +53,7 @@ val _ = session := {chapter = chapter, name = name}; val _ = session_finished := false; in - Present.init build info info_path (if doc = "false" then "" else doc) + Present.init symbols build info info_path (if doc = "false" then "" else doc) doc_output doc_variants doc_files graph_file (chapter, name) verbose end; diff -r 3907f20bef8c -r ddca85598c65 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Fri Oct 09 21:20:43 2015 +0200 +++ b/src/Pure/PIDE/session.scala Sat Oct 10 16:21:34 2015 +0200 @@ -494,7 +494,6 @@ 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 => diff -r 3907f20bef8c -r ddca85598c65 src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Fri Oct 09 21:20:43 2015 +0200 +++ b/src/Pure/Thy/html.ML Sat Oct 10 16:21:34 2015 +0200 @@ -6,23 +6,16 @@ signature HTML = sig - val reset_symbols: unit -> unit - val init_symbols: (string * int) list -> unit - val present_span: Keyword.keywords -> Command_Span.span -> Output.output + type symbols + val make_symbols: (string * int) list -> symbols + val no_symbols: symbols + val present_span: symbols -> Keyword.keywords -> Command_Span.span -> Output.output type text = string - val plain: string -> text - val name: string -> text - val keyword: string -> text - val command: string -> text - val href_name: string -> text -> text - val href_path: Url.T -> text -> text - val href_opt_path: Url.T option -> text -> text - val para: text -> text - val begin_document: string -> text + val begin_document: symbols -> string -> text val end_document: text - val begin_session_index: string -> Url.T -> (Url.T * string) list -> text - val theory_entry: Url.T * string -> text - val theory: string -> (Url.T option * string) list -> text -> text + val begin_session_index: symbols -> string -> Url.T -> (Url.T * string) list -> text + val theory_entry: symbols -> Url.T * string -> text + val theory: symbols -> string -> (Url.T option * string) list -> text -> text end; structure HTML: HTML = @@ -38,70 +31,66 @@ (* symbol output *) +abstype symbols = Symbols of string Symtab.table +with + +fun make_symbols codes = + let + val mapping = + map (apsnd (fn c => "&#" ^ Markup.print_int c ^ ";")) codes @ + [("'", "'"), + ("\\<^bsub>", hidden "⇘" ^ ""), + ("\\<^esub>", hidden "⇙" ^ ""), + ("\\<^bsup>", hidden "⇗" ^ ""), + ("\\<^esup>", hidden "⇖" ^ "")]; + in Symbols (fold Symtab.update mapping Symtab.empty) end; + +val no_symbols = make_symbols []; + +fun output_sym (Symbols tab) s = + if Symbol.is_raw s then Symbol.decode_raw s + else + (case Symtab.lookup tab s of + SOME x => x + | NONE => XML.text s); + +end; + local -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"); - -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_markup (bg, en) symbols s1 s2 = + hidden s1 ^ enclose bg en (output_sym symbols s2); 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) = +fun output_syms _ [] result = implode (rev result) + | output_syms symbols (s1 :: rest) result = 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 (s, r) = + if s1 = "\\<^sub>" then (output_sub symbols "⇩" s2, ss) + else if s1 = "\\<^sup>" then (output_sup symbols "⇧" s2, ss) + else if s1 = "\\<^bold>" then (output_bold symbols "❙" s2, ss) + else (output_sym symbols s1, rest); + in output_syms symbols r (s :: result) end; in -fun output_width str = output_syms (Symbol.explode str) ([], 0); -val output = #1 o output_width; - -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; +fun output symbols str = output_syms symbols (Symbol.explode str) []; end; (* presentation *) -fun present_token keywords tok = - fold_rev (uncurry enclose o span o #1) - (Token.markups keywords tok) (output (Token.unparse tok)); - -fun present_span keywords = - implode o map (present_token keywords) o Command_Span.content; +fun present_span symbols keywords = + let + fun present_token tok = + fold_rev (uncurry enclose o span o #1) + (Token.markups keywords tok) (output symbols (Token.unparse tok)); + in implode o map present_token o Command_Span.content end; @@ -112,10 +101,9 @@ (* atoms *) -val plain = output; -val name = enclose "" "" o output; -val keyword = enclose "" "" o output; -val command = enclose "" "" o output; +val name = enclose "" "" oo output; +val keyword = enclose "" "" oo output; +val command = enclose "" "" oo output; (* misc *) @@ -131,41 +119,42 @@ (* document *) -fun begin_document title = +fun begin_document symbols title = "\n\ \\n\ \\n\ \\n\ \\n\ - \" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "\n\ + \" ^ output symbols (title ^ " (" ^ Distribution.version ^ ")") ^ "\n\ \\n\ \\n\ \\n\ \\n\ \
\ - \

" ^ plain title ^ "

\n"; + \

" ^ output symbols title ^ "

\n"; val end_document = "\n
\n\n\n"; (* session index *) -fun begin_session_index session graph docs = - begin_document ("Session " ^ plain session) ^ +fun begin_session_index symbols session graph docs = + begin_document symbols ("Session " ^ output symbols session) ^ para ("View " ^ href_path graph "theory dependencies" ^ implode (map (fn (p, name) => "
\nView " ^ href_path p name) docs)) ^ "\n\n
\n

Theories

\n
\n
\n
" "
\n" txt ^ end_document; diff -r 3907f20bef8c -r ddca85598c65 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Fri Oct 09 21:20:43 2015 +0200 +++ b/src/Pure/Thy/present.ML Sat Oct 10 16:21:34 2015 +0200 @@ -10,7 +10,7 @@ val session_graph: string -> (string -> bool) -> theory -> Graph_Display.entry list val document_enabled: string -> bool val document_variants: string -> (string * string) list - val init: bool -> bool -> Path.T -> string -> string -> (string * string) list -> + val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list -> (Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit val finish: unit -> unit val theory_output: string -> string -> unit @@ -138,15 +138,15 @@ (* session_info *) type session_info = - {name: string, chapter: string, info_path: Path.T, info: bool, doc_format: string, - doc_output: Path.T option, doc_files: (Path.T * Path.T) list, graph_file: Path.T, - documents: (string * string) list, verbose: bool, readme: Path.T option}; + {symbols: HTML.symbols, name: string, chapter: string, info_path: Path.T, info: bool, + doc_format: string, doc_output: Path.T option, doc_files: (Path.T * Path.T) list, + graph_file: Path.T, documents: (string * string) list, verbose: bool, readme: Path.T option}; fun make_session_info - (name, chapter, info_path, info, doc_format, doc_output, doc_files, + (symbols, name, chapter, info_path, info, doc_format, doc_output, doc_files, graph_file, documents, verbose, readme) = - {name = name, chapter = chapter, info_path = info_path, info = info, doc_format = doc_format, - doc_output = doc_output, doc_files = doc_files, graph_file = graph_file, + {symbols = symbols, name = name, chapter = chapter, info_path = info_path, info = info, + doc_format = doc_format, doc_output = doc_output, doc_files = doc_files, graph_file = graph_file, documents = documents, verbose = verbose, readme = readme}: session_info; @@ -181,7 +181,7 @@ (* init session *) -fun init build info info_path doc document_output doc_variants doc_files graph_file +fun init symbols build info info_path doc document_output doc_variants doc_files graph_file (chapter, name) verbose = if not build andalso not info andalso doc = "" then (Synchronized.change browser_info (K empty_browser_info); session_info := NONE) @@ -204,10 +204,10 @@ map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents; in session_info := - SOME (make_session_info (name, chapter, info_path, info, doc, + SOME (make_session_info (symbols, name, chapter, info_path, info, doc, doc_output, doc_files, graph_file, documents, verbose, readme)); Synchronized.change browser_info (K empty_browser_info); - add_html_index (0, HTML.begin_session_index name (Url.File session_graph_path) docs) + add_html_index (0, HTML.begin_session_index symbols name (Url.File session_graph_path) docs) end; @@ -320,7 +320,7 @@ end; fun begin_theory update_time mk_text thy = - with_session_info thy (fn {name = session_name, chapter, ...} => + with_session_info thy (fn {symbols, name = session_name, chapter, ...} => let val name = Context.theory_name thy; val parents = Theory.parents_of thy; @@ -328,10 +328,10 @@ val parent_specs = parents |> map (fn parent => (Option.map Url.File (theory_link (chapter, session_name) parent), (Context.theory_name parent))); - val html_source = HTML.theory name parent_specs (mk_text ()); + val html_source = HTML.theory symbols name parent_specs (mk_text ()); in init_theory_info name (make_theory_info ("", html_source)); - add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name)); + add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name)); add_tex_index (update_time, Latex.theory_entry name); Browser_Info.put {chapter = chapter, name = session_name} thy end); diff -r 3907f20bef8c -r ddca85598c65 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Fri Oct 09 21:20:43 2015 +0200 +++ b/src/Pure/Thy/thy_info.ML Sat Oct 10 16:21:34 2015 +0200 @@ -14,8 +14,10 @@ val master_directory: string -> Path.T val remove_thy: string -> unit val use_theories: - {document: bool, last_timing: Toplevel.transition -> Time.time option, master_dir: Path.T} -> - (string * Position.T) list -> unit + {document: bool, + symbols: HTML.symbols, + last_timing: Toplevel.transition -> Time.time option, + master_dir: Path.T} -> (string * Position.T) list -> unit val use_thys: (string * Position.T) list -> unit val use_thy: string * Position.T -> unit val script_thy: Position.T -> string -> theory -> theory @@ -237,7 +239,8 @@ fun required_by _ [] = "" | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; -fun load_thy document last_timing initiators update_time deps text (name, pos) keywords parents = +fun load_thy document symbols last_timing + initiators update_time deps text (name, pos) keywords parents = let val _ = remove_thy name; val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators); @@ -256,7 +259,7 @@ val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path); val (theory, present, weight) = - Resources.load_thy document last_timing update_time dir header text_pos text + Resources.load_thy document symbols last_timing update_time dir header text_pos text (if name = Context.PureN then [ML_Context.the_global_context ()] else parents); fun commit () = update_thy deps theory; in @@ -283,9 +286,9 @@ in -fun require_thys document last_timing initiators dir strs tasks = - fold_map (require_thy document last_timing initiators dir) strs tasks |>> forall I -and require_thy document last_timing initiators dir (str, require_pos) tasks = +fun require_thys document symbols last_timing initiators dir strs tasks = + fold_map (require_thy document symbols last_timing initiators dir) strs tasks |>> forall I +and require_thy document symbols last_timing initiators dir (str, require_pos) tasks = let val path = Path.expand (Path.explode str); val name = Path.implode (Path.base path); @@ -315,7 +318,7 @@ val parents = map (base_name o #1) imports; val (parents_current, tasks') = - require_thys document last_timing (name :: initiators) + require_thys document symbols last_timing (name :: initiators) (Path.append dir (master_dir (Option.map #1 deps))) imports tasks; val all_current = current andalso parents_current; @@ -328,7 +331,7 @@ let val update_time = serial (); val load = - load_thy document last_timing initiators update_time dep + load_thy document symbols last_timing initiators update_time dep text (name, theory_pos) keywords; in Task (node_name, parents, load) end); @@ -341,10 +344,14 @@ (* use_thy *) -fun use_theories {document, last_timing, master_dir} imports = - schedule_tasks (snd (require_thys document last_timing [] master_dir imports String_Graph.empty)); +fun use_theories {document, symbols, last_timing, master_dir} imports = + schedule_tasks + (snd (require_thys document symbols last_timing [] master_dir imports String_Graph.empty)); -val use_thys = use_theories {document = false, last_timing = K NONE, master_dir = Path.current}; +val use_thys = + use_theories + {document = false, symbols = HTML.no_symbols, last_timing = K NONE, master_dir = Path.current}; + val use_thy = use_thys o single; diff -r 3907f20bef8c -r ddca85598c65 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Fri Oct 09 21:20:43 2015 +0200 +++ b/src/Pure/Tools/build.ML Sat Oct 10 16:21:34 2015 +0200 @@ -97,7 +97,7 @@ (* build *) -fun build_theories last_timing master_dir (options, thys) = +fun build_theories symbols last_timing master_dir (options, thys) = let val condition = space_explode "," (Options.string options "condition"); val conds = filter_out (can getenv_strict) condition; @@ -106,6 +106,7 @@ (Options.set_default options; (Thy_Info.use_theories { document = Present.document_enabled (Options.string options "document"), + symbols = symbols, last_timing = last_timing, master_dir = master_dir} |> Unsynchronized.setmp print_mode @@ -133,12 +134,14 @@ ((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))) end; - val _ = HTML.init_symbols symbol_codes; + val symbols = HTML.make_symbols symbol_codes; val _ = Options.set_default options; val _ = writeln ("\fSession.name = " ^ name); val _ = - Session.init do_output + Session.init + symbols + do_output (Options.bool options "browser_info") (Path.explode browser_info) (Options.string options "document") @@ -153,7 +156,7 @@ val res1 = theories |> - (List.app (build_theories last_timing Path.current) + (List.app (build_theories symbols last_timing Path.current) |> session_timing name verbose |> Unsynchronized.setmp Output.protocol_message_fn protocol_message |> Multithreading.max_threads_setmp (Options.int options "threads") @@ -161,7 +164,6 @@ 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); @@ -171,15 +173,19 @@ val _ = Isabelle_Process.protocol_command "build_theories" - (fn [id, master_dir, theories_yxml] => + (fn [id, symbol_codes_yxml, master_dir, theories_yxml] => let + val symbols = + YXML.parse_body symbol_codes_yxml + |> let open XML.Decode in list (pair string int) end + |> HTML.make_symbols; val theories = YXML.parse_body theories_yxml |> let open XML.Decode in list (pair Options.decode (list (string #> rpair Position.none))) end; val res1 = Exn.capture (fn () => - theories |> List.app (build_theories (K NONE) (Path.explode master_dir))) (); + theories |> List.app (build_theories symbols (K NONE) (Path.explode master_dir))) (); val res2 = Exn.capture Session.shutdown (); val result = (Par_Exn.release_all [res1, res2]; "") handle exn =>