--- 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--- 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)) }--- 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)--- 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;
--- 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 =>--- 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 "⇘" ^ "<sub>"),
+ ("\\<^esub>", hidden "⇙" ^ "</sub>"),
+ ("\\<^bsup>", hidden "⇗" ^ "<sup>"),
+ ("\\<^esup>", hidden "⇖" ^ "</sup>")];
+ 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 ("<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) =
+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 "⇘" ^ "<sub>")),
- ("\\<^esub>", (0, hidden "⇙" ^ "</sub>")),
- ("\\<^bsup>", (0, hidden "⇗" ^ "<sup>")),
- ("\\<^esup>", (0, hidden "⇖" ^ "</sup>"))];
- 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 "<span class=\"name\">" "</span>" o output;
-val keyword = enclose "<span class=\"keyword\">" "</span>" o output;
-val command = enclose "<span class=\"command\">" "</span>" o output;
+val name = enclose "<span class=\"name\">" "</span>" oo output;
+val keyword = enclose "<span class=\"keyword\">" "</span>" oo output;
+val command = enclose "<span class=\"command\">" "</span>" oo output;
(* misc *)
@@ -131,41 +119,42 @@
(* document *)
-fun begin_document title =
+fun begin_document symbols title =
"<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n\
\<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \
\\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\
\<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\
\<head>\n\
\<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n\
- \<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
+ \<title>" ^ output symbols (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
\<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n\
\</head>\n\
\\n\
\<body>\n\
\<div class=\"head\">\
- \<h1>" ^ plain title ^ "</h1>\n";
+ \<h1>" ^ output symbols title ^ "</h1>\n";
val end_document = "\n</div>\n</body>\n</html>\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) => "<br/>\nView " ^ href_path p name) docs)) ^
"\n</div>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
-fun theory_entry (p, s) = "<li>" ^ href_path p (plain s) ^ "</li>\n";
+fun theory_entry symbols (p, s) = "<li>" ^ href_path p (output symbols s) ^ "</li>\n";
(* theory *)
-fun theory A Bs txt =
- begin_document ("Theory " ^ A) ^ "\n" ^
- command "theory" ^ " " ^ name A ^ "<br/>\n" ^
- keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs) ^
+fun theory symbols A Bs txt =
+ begin_document symbols ("Theory " ^ A) ^ "\n" ^
+ command symbols "theory" ^ " " ^ name symbols A ^ "<br/>\n" ^
+ keyword symbols "imports" ^ " " ^
+ space_implode " " (map (uncurry href_opt_path o apsnd (name symbols)) Bs) ^
"<br/>\n" ^
enclose "\n</div>\n<div class=\"source\">\n<pre class=\"source\">" "</pre>\n" txt ^
end_document;--- 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);--- 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;
--- 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 =>