diff --git a/src/Pure/PIDE/protocol.ML b/src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML +++ b/src/Pure/PIDE/protocol.ML @@ -1,178 +1,178 @@ (* Title: Pure/PIDE/protocol.ML Author: Makarius Protocol message formats for interactive proof documents. *) structure Protocol: sig end = struct val _ = Protocol_Command.define "Prover.echo" (fn args => List.app writeln args); val _ = Protocol_Command.define "Prover.stop" (fn rc :: msgs => (List.app Output.system_message msgs; raise Protocol_Command.STOP (Value.parse_int rc))); val _ = Protocol_Command.define "Prover.options" (fn [options_yxml] => (Options.set_default (Options.decode (YXML.parse_body options_yxml)); Isabelle_Process.init_options_interactive ())); val _ = - Protocol_Command.define "Prover.init_session" + Protocol_Command.define_bytes "Prover.init_session" (fn [yxml] => Resources.init_session_yxml yxml); val _ = Protocol_Command.define "Document.define_blob" (fn [digest, content] => Document.change_state (Document.define_blob digest content)); fun decode_command id name parents_xml blobs_xml toks_xml sources : Document.command = let open XML.Decode; val parents = list string parents_xml; val (blobs_digests, blobs_index) = blobs_xml |> let val message = YXML.string_of_body o Protocol_Message.command_positions id; val blob = triple string string (option string) #> (fn (a, b, c) => {file_node = a, src_path = Path.explode b, digest = c}); in pair (list (variant [fn ([], a) => Exn.Res (blob a), fn ([], a) => Exn.Exn (ERROR (message a))])) int end; val toks = list (pair int int) toks_xml; in {command_id = Document_ID.parse id, name = name, parents = parents, blobs_digests = blobs_digests, blobs_index = blobs_index, tokens = toks ~~ sources} end; fun commands_accepted ids = Output.protocol_message Markup.commands_accepted [[XML.Text (space_implode "," ids)]]; val _ = Protocol_Command.define "Document.define_command" (fn id :: name :: parents :: blobs :: toks :: sources => let val command = decode_command id name (YXML.parse_body parents) (YXML.parse_body blobs) (YXML.parse_body toks) sources; val _ = Document.change_state (Document.define_command command); in commands_accepted [id] end); val _ = Protocol_Command.define "Document.define_commands" (fn args => let fun decode arg = let open XML.Decode; val (id, (name, (parents_xml, (blobs_xml, (toks_xml, sources))))) = pair string (pair string (pair I (pair I (pair I (list string))))) (YXML.parse_body arg); in decode_command id name parents_xml blobs_xml toks_xml sources end; val commands = map decode args; val _ = Document.change_state (fold Document.define_command commands); in commands_accepted (map (Value.print_int o #command_id) commands) end); val _ = Protocol_Command.define "Document.discontinue_execution" (fn [] => Execution.discontinue ()); val _ = Protocol_Command.define "Document.cancel_exec" (fn [exec_id] => Execution.cancel (Document_ID.parse exec_id)); val _ = Protocol_Command.define "Document.update" (Future.task_context "Document.update" (Future.new_group NONE) (fn old_id_string :: new_id_string :: consolidate_yxml :: edits_yxml => Document.change_state (fn state => let val old_id = Document_ID.parse old_id_string; val new_id = Document_ID.parse new_id_string; val consolidate = YXML.parse_body consolidate_yxml |> let open XML.Decode in list string end; val edits = edits_yxml |> map (YXML.parse_body #> let open XML.Decode in pair string (variant [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), fn ([], a) => let val (master, (name, (imports, (keywords, errors)))) = pair string (pair string (pair (list string) (pair (list (pair string (pair string (list string)))) (list YXML.string_of_body)))) a; val imports' = map (rpair Position.none) imports; val keywords' = map (fn (x, y) => ((x, Position.none), Keyword.command_spec y)) keywords; val header = Thy_Header.make (name, Position.none) imports' keywords'; in Document.Deps {master = master, header = header, errors = errors} end, fn (a :: b, c) => Document.Perspective (bool_atom a, map int_atom b, list (pair int (pair string (list string))) c)]) end); val _ = Execution.discontinue (); val (edited, removed, assign_update, state') = Document.update old_id new_id edits consolidate state; val _ = (singleton o Future.forks) {name = "Document.update/remove", group = NONE, deps = Execution.snapshot removed, pri = Task_Queue.urgent_pri + 2, interrupts = false} (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed)); val _ = Output.protocol_message Markup.assign_update [(new_id, edited, assign_update) |> let open XML.Encode; fun encode_upd (a, bs) = string (space_implode "," (map Value.print_int (a :: bs))); in triple int (list string) (list encode_upd) end]; in Document.start_execution state' end))); val _ = Protocol_Command.define "Document.remove_versions" (fn [versions_yxml] => Document.change_state (fn state => let val versions = YXML.parse_body versions_yxml |> let open XML.Decode in list int end; val state1 = Document.remove_versions versions state; val _ = Output.protocol_message Markup.removed_versions [[XML.Text (versions_yxml)]]; in state1 end)); val _ = Protocol_Command.define "Document.dialog_result" (fn [serial, result] => Active.dialog_result (Value.parse_int serial) result handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn); val _ = Protocol_Command.define "ML_Heap.full_gc" (fn [] => ML_Heap.full_gc ()); val _ = Protocol_Command.define "ML_Heap.share_common_data" (fn [] => ML_Heap.share_common_data ()); end; diff --git a/src/Pure/PIDE/resources.ML b/src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML +++ b/src/Pure/PIDE/resources.ML @@ -1,444 +1,444 @@ (* Title: Pure/PIDE/resources.ML Author: Makarius Resources for theories and auxiliary files. *) signature RESOURCES = sig val default_qualifier: string val init_session: {session_positions: (string * Properties.T) list, session_directories: (string * string) list, bibtex_entries: (string * string list) list, command_timings: Properties.T list, load_commands: (string * Position.T) list, scala_functions: (string * ((bool * bool) * Position.T)) list, global_theories: (string * string) list, loaded_theories: string list} -> unit - val init_session_yxml: string -> unit + val init_session_yxml: Bytes.T -> unit val init_session_env: unit -> unit val finish_session_base: unit -> unit val global_theory: string -> string option val loaded_theory: string -> bool val check_session: Proof.context -> string * Position.T -> string val last_timing: Toplevel.transition -> Time.time val check_load_command: Proof.context -> string * Position.T -> string val check_scala_function: Proof.context -> string * Position.T -> string * (bool * bool) val master_directory: theory -> Path.T val imports_of: theory -> (string * Position.T) list val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory val thy_path: Path.T -> Path.T val theory_qualifier: string -> string val theory_bibtex_entries: string -> string list val find_theory_file: string -> Path.T option val import_name: string -> Path.T -> string -> {node_name: Path.T, master_dir: Path.T, theory_name: string} val check_thy: Path.T -> string -> {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T, imports: (string * Position.T) list, keywords: Thy_Header.keywords} val parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list) parser val parse_file: (theory -> Token.file) parser val provide: Path.T * SHA1.digest -> theory -> theory val provide_file: Token.file -> theory -> theory val provide_parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list * theory) parser val provide_parse_file: (theory -> Token.file * theory) parser val loaded_files_current: theory -> bool val check_path: Proof.context -> Path.T option -> Input.source -> Path.T val check_file: Proof.context -> Path.T option -> Input.source -> Path.T val check_dir: Proof.context -> Path.T option -> Input.source -> Path.T val check_session_dir: Proof.context -> Path.T option -> Input.source -> Path.T end; structure Resources: RESOURCES = struct (* command timings *) type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name, time*) val empty_timings: timings = Symtab.empty; fun update_timings props = (case Markup.parse_command_timing_properties props of SOME ({file, offset, name}, time) => Symtab.map_default (file, Inttab.empty) (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time))) | NONE => I); fun make_timings command_timings = fold update_timings command_timings empty_timings; fun approximative_id name pos = (case (Position.file_of pos, Position.offset_of pos) of (SOME file, SOME offset) => if name = "" then NONE else SOME {file = file, offset = offset, name = name} | _ => NONE); fun get_timings timings tr = (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of SOME {file, offset, name} => (case Symtab.lookup timings file of SOME offsets => (case Inttab.lookup offsets offset of SOME (name', time) => if name = name' then SOME time else NONE | NONE => NONE) | NONE => NONE) | NONE => NONE) |> the_default Time.zeroTime; (* session base *) val default_qualifier = "Draft"; type entry = {pos: Position.T, serial: serial}; fun make_entry props : entry = {pos = Position.of_properties props, serial = serial ()}; val empty_session_base = ({session_positions = []: (string * entry) list, session_directories = Symtab.empty: Path.T list Symtab.table, bibtex_entries = Symtab.empty: string list Symtab.table, timings = empty_timings, load_commands = []: (string * Position.T) list, scala_functions = Symtab.empty: ((bool * bool) * Position.T) Symtab.table}, {global_theories = Symtab.empty: string Symtab.table, loaded_theories = Symtab.empty: unit Symtab.table}); val global_session_base = Synchronized.var "Sessions.base" empty_session_base; fun init_session {session_positions, session_directories, bibtex_entries, command_timings, load_commands, scala_functions, global_theories, loaded_theories} = Synchronized.change global_session_base (fn _ => ({session_positions = sort_by #1 (map (apsnd make_entry) session_positions), session_directories = Symtab.build (session_directories |> fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir))), bibtex_entries = Symtab.make bibtex_entries, timings = make_timings command_timings, load_commands = load_commands, scala_functions = Symtab.make scala_functions}, {global_theories = Symtab.make global_theories, loaded_theories = Symtab.make_set loaded_theories})); fun init_session_yxml yxml = let val (session_positions, (session_directories, (bibtex_entries, (command_timings, (load_commands, (scala_functions, (global_theories, loaded_theories))))))) = - YXML.parse_body yxml |> + YXML.parse_body_bytes yxml |> let open XML.Decode in (pair (list (pair string properties)) (pair (list (pair string string)) (pair (list (pair string (list string))) (pair (list properties) (pair (list (pair string properties)) (pair (list (pair string (pair (pair bool bool) properties))) (pair (list (pair string string)) (list string)))))))) end; in init_session {session_positions = session_positions, session_directories = session_directories, bibtex_entries = bibtex_entries, command_timings = command_timings, load_commands = (map o apsnd) Position.of_properties load_commands, scala_functions = (map o apsnd o apsnd) Position.of_properties scala_functions, global_theories = global_theories, loaded_theories = loaded_theories} end; fun init_session_env () = (case getenv "ISABELLE_INIT_SESSION" of "" => () | name => - try File.read (Path.explode name) + try Bytes.read (Path.explode name) |> Option.app init_session_yxml); val _ = init_session_env (); fun finish_session_base () = Synchronized.change global_session_base (apfst (K (#1 empty_session_base))); fun get_session_base f = f (Synchronized.value global_session_base); fun get_session_base1 f = get_session_base (f o #1); fun get_session_base2 f = get_session_base (f o #2); fun global_theory a = Symtab.lookup (get_session_base2 #global_theories) a; fun loaded_theory a = Symtab.defined (get_session_base2 #loaded_theories) a; fun check_session ctxt arg = Completion.check_item "session" (fn (name, {pos, serial}) => Position.make_entity_markup {def = false} serial Markup.sessionN (name, pos)) (get_session_base1 #session_positions) ctxt arg; fun last_timing tr = get_timings (get_session_base1 #timings) tr; fun check_load_command ctxt arg = Completion.check_entity Markup.load_commandN (get_session_base1 #load_commands) ctxt arg; (* Scala functions *) fun check_scala_function ctxt arg = let val table = get_session_base1 #scala_functions; val funs = Symtab.fold (fn (a, (_, pos)) => cons (a, pos)) table [] |> sort_by #1; val name = Completion.check_entity Markup.scala_functionN funs ctxt arg; val flags = #1 (the (Symtab.lookup table name)); in (name, flags) end; val _ = Theory.setup (Document_Output.antiquotation_verbatim_embedded \<^binding>\scala_function\ (Scan.lift Parse.embedded_position) (#1 oo check_scala_function) #> ML_Antiquotation.inline_embedded \<^binding>\scala_function\ (Args.context -- Scan.lift Parse.embedded_position >> (uncurry check_scala_function #> #1 #> ML_Syntax.print_string)) #> ML_Antiquotation.value_embedded \<^binding>\scala\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, arg) => let val (name, (single, bytes)) = check_scala_function ctxt arg; val func = (if single then "Scala.function1" else "Scala.function") ^ (if bytes then "_bytes" else ""); in ML_Syntax.atomic (func ^ " " ^ ML_Syntax.print_string name) end))); (* manage source files *) type files = {master_dir: Path.T, (*master directory of theory source*) imports: (string * Position.T) list, (*source specification of imports*) provided: (Path.T * SHA1.digest) list}; (*source path, digest*) fun make_files (master_dir, imports, provided): files = {master_dir = master_dir, imports = imports, provided = provided}; structure Files = Theory_Data ( type T = files; val empty = make_files (Path.current, [], []); fun merge ({master_dir, imports, provided = provided1}, {provided = provided2, ...}) = let val provided' = Library.merge (op =) (provided1, provided2) in make_files (master_dir, imports, provided') end ); fun map_files f = Files.map (fn {master_dir, imports, provided} => make_files (f (master_dir, imports, provided))); val master_directory = #master_dir o Files.get; val imports_of = #imports o Files.get; fun begin_theory master_dir {name, imports, keywords} parents = let val thy = Theory.begin_theory name parents |> map_files (fn _ => (Path.explode (Path.implode_symbolic master_dir), imports, [])) |> Thy_Header.add_keywords keywords; val ctxt = Proof_Context.init_global thy; val _ = List.app (ignore o check_load_command ctxt o #load_command o #2) keywords; in thy end; (* theory files *) val thy_path = Path.ext "thy"; fun theory_qualifier theory = (case global_theory theory of SOME qualifier => qualifier | NONE => Long_Name.qualifier theory); fun theory_name qualifier theory = if Long_Name.is_qualified theory orelse is_some (global_theory theory) then theory else Long_Name.qualify qualifier theory; fun theory_bibtex_entries theory = Symtab.lookup_list (get_session_base1 #bibtex_entries) (theory_qualifier theory); fun find_theory_file thy_name = let val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name)); val session = theory_qualifier thy_name; val dirs = Symtab.lookup_list (get_session_base1 #session_directories) session; in dirs |> get_first (fn dir => let val path = dir + thy_file in if File.is_file path then SOME path else NONE end) end; fun make_theory_node node_name theory = {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory}; fun loaded_theory_node theory = {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}; fun import_name qualifier dir s = let val theory = theory_name qualifier (Thy_Header.import_name s); fun theory_node () = make_theory_node (File.full_path dir (thy_path (Path.expand (Path.explode s)))) theory; in if not (Thy_Header.is_base_name s) then theory_node () else if loaded_theory theory then loaded_theory_node theory else (case find_theory_file theory of SOME node_name => make_theory_node node_name theory | NONE => if Long_Name.is_qualified s then loaded_theory_node theory else theory_node ()) end; fun check_file dir file = File.check_file (File.full_path dir file); fun check_thy dir thy_name = let val thy_base_name = Long_Name.base_name thy_name; val master_file = (case find_theory_file thy_name of SOME path => check_file Path.current path | NONE => check_file dir (thy_path (Path.basic thy_base_name))); val text = File.read master_file; val {name = (name, pos), imports, keywords} = Thy_Header.read (Path.position master_file) text; val _ = thy_base_name <> name andalso error ("Bad theory name " ^ quote name ^ " for file " ^ Path.print (Path.base master_file) ^ Position.here pos); in {master = (master_file, SHA1.digest text), text = text, theory_pos = pos, imports = imports, keywords = keywords} end; (* load files *) fun parse_files make_paths = Scan.ahead Parse.not_eof -- Parse.path_input >> (fn (tok, source) => fn thy => (case Token.get_files tok of [] => let val master_dir = master_directory thy; val name = Input.string_of source; val pos = Input.pos_of source; val delimited = Input.is_delimited source; val src_paths = make_paths (Path.explode name); in map (Command.read_file master_dir pos delimited) src_paths end | files => map Exn.release files)); val parse_file = parse_files single >> (fn f => f #> the_single); fun provide (src_path, id) = map_files (fn (master_dir, imports, provided) => if AList.defined (op =) provided src_path then error ("Duplicate use of source file: " ^ Path.print src_path) else (master_dir, imports, (src_path, id) :: provided)); fun provide_file (file: Token.file) = provide (#src_path file, #digest file); fun provide_parse_files make_paths = parse_files make_paths >> (fn files => fn thy => let val fs = files thy; val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy; in (fs, thy') end); val provide_parse_file = provide_parse_files single >> (fn f => f #>> the_single); fun load_file thy src_path = let val full_path = check_file (master_directory thy) src_path; val text = File.read full_path; val id = SHA1.digest text; in ((full_path, id), text) end; fun loaded_files_current thy = #provided (Files.get thy) |> forall (fn (src_path, id) => (case try (load_file thy) src_path of NONE => false | SOME ((_, id'), _) => id = id')); (* formal check *) fun formal_check check_file ctxt opt_dir source = let val name = Input.string_of source; val pos = Input.pos_of source; val delimited = Input.is_delimited source; val _ = Context_Position.report ctxt pos (Markup.language_path delimited); fun err msg = error (msg ^ Position.here pos); val dir = (case opt_dir of SOME dir => dir | NONE => master_directory (Proof_Context.theory_of ctxt)); val path = dir + Path.explode name handle ERROR msg => err msg; val _ = Path.expand path handle ERROR msg => err msg; val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path)); val _ : Path.T = check_file path handle ERROR msg => err msg; in path end; val check_path = formal_check I; val check_file = formal_check File.check_file; val check_dir = formal_check File.check_dir; fun check_session_dir ctxt opt_dir s = let val dir = Path.expand (check_dir ctxt opt_dir s); val ok = File.is_file (dir + Path.explode("ROOT")) orelse File.is_file (dir + Path.explode("ROOTS")); in if ok then dir else error ("Bad session root directory (missing ROOT or ROOTS): " ^ Path.print dir ^ Position.here (Input.pos_of s)) end; (* antiquotations *) local fun document_antiq (check: Proof.context -> Path.T option -> Input.source -> Path.T) = Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) => (check ctxt NONE source; Latex.string (Latex.output_ascii_breakable "/" (Input.string_of source)) |> Latex.macro "isatt")); fun ML_antiq check = Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) => check ctxt (SOME Path.current) source |> ML_Syntax.print_path); in val _ = Theory.setup (Document_Output.antiquotation_verbatim_embedded \<^binding>\session\ (Scan.lift Parse.embedded_position) check_session #> Document_Output.antiquotation_raw_embedded \<^binding>\path\ (document_antiq check_path) (K I) #> Document_Output.antiquotation_raw_embedded \<^binding>\file\ (document_antiq check_file) (K I) #> Document_Output.antiquotation_raw_embedded \<^binding>\dir\ (document_antiq check_dir) (K I) #> ML_Antiquotation.value_embedded \<^binding>\path\ (ML_antiq check_path) #> ML_Antiquotation.value_embedded \<^binding>\file\ (ML_antiq check_file) #> ML_Antiquotation.value_embedded \<^binding>\dir\ (ML_antiq check_dir) #> ML_Antiquotation.value_embedded \<^binding>\path_binding\ (Scan.lift (Parse.position Parse.path) >> (ML_Syntax.print_path_binding o Path.explode_binding)) #> ML_Antiquotation.value \<^binding>\master_dir\ (Args.theory >> (ML_Syntax.print_path o master_directory))); end; end; diff --git a/src/Pure/PIDE/yxml.ML b/src/Pure/PIDE/yxml.ML --- a/src/Pure/PIDE/yxml.ML +++ b/src/Pure/PIDE/yxml.ML @@ -1,175 +1,188 @@ (* Title: Pure/PIDE/yxml.ML Author: Makarius Efficient text representation of XML trees using extra characters X and Y -- no escaping, may nest marked text verbatim. Suitable for direct inlining into plain text. Markup ...body... is encoded as: X Y name Y att=val ... X ... body ... X Y X *) signature YXML = sig val X: Symbol.symbol val Y: Symbol.symbol val embed_controls: string -> string val detect: string -> bool val traverse: (string -> 'a -> 'a) -> XML.tree -> 'a -> 'a val tree_size: XML.tree -> int val body_size: XML.body -> int val string_of_body: XML.body -> string val string_of: XML.tree -> string val write_body: Path.T -> XML.body -> unit val output_markup: Markup.T -> string * string val output_markup_elem: Markup.T -> (string * string) * string val parse_body: string -> XML.body + val parse_body_bytes: Bytes.T -> XML.body val parse: string -> XML.tree + val parse_bytes: Bytes.T -> XML.tree val content_of: string -> string val is_wellformed: string -> bool end; structure YXML: YXML = struct (** string representation **) (* idempotent recoding of certain low ASCII control characters *) fun pseudo_utf8 c = if Symbol.is_ascii_control c then chr 192 ^ chr (128 + ord c) else c; fun embed_controls str = if exists_string Symbol.is_ascii_control str then translate_string pseudo_utf8 str else str; (* markers *) val X_char = Char.chr 5; val Y_char = Char.chr 6; val X = String.str X_char; val Y = String.str Y_char; val XY = X ^ Y; val XYX = XY ^ X; fun detect s = Char.contains s X_char orelse Char.contains s Y_char; (* traverse *) fun traverse string = let fun attrib (a, x) = string Y #> string a #> string "=" #> string x; fun tree (XML.Elem (markup as (name, atts), ts)) = if Markup.is_empty markup then fold tree ts else string XY #> string name #> fold attrib atts #> string X #> fold tree ts #> string XYX | tree (XML.Text s) = string s; in tree end; fun tree_size tree = traverse (Integer.add o size) tree 0; fun body_size body = fold (Integer.add o tree_size) body 0; (* output *) val string_of_body = Buffer.build_content o fold (traverse Buffer.add); val string_of = string_of_body o single; fun write_body path body = path |> File_Stream.open_output (fn file => fold (traverse (fn s => fn () => File_Stream.output file s)) body ()); (* markup elements *) val Z = chr 0; val Z_text = [XML.Text Z]; fun output_markup (markup as (name, atts)) = if Markup.is_empty markup then Markup.no_output else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX); fun output_markup_elem markup = let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text))) in ((bg1, bg2), en) end; (** efficient YXML parsing **) local (* splitting *) val split_string = Substring.full #> Substring.tokens (fn c => c = X_char) #> map (Substring.fields (fn c => c = Y_char) #> map Substring.string); +val split_bytes = + Bytes.space_explode X + #> filter (fn "" => false | _ => true) + #> map (space_explode Y); + (* structural errors *) fun err msg = raise Fail ("Malformed YXML: " ^ msg); fun err_attribute () = err "bad attribute"; fun err_element () = err "bad element"; fun err_unbalanced "" = err "unbalanced element" | err_unbalanced name = err ("unbalanced element " ^ quote name); (* stack operations *) fun add x ((elem, body) :: pending) = (elem, x :: body) :: pending; fun push "" _ _ = err_element () | push name atts pending = ((name, atts), []) :: pending; fun pop ((("", _), _) :: _) = err_unbalanced "" | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending; (* parsing *) fun parse_attrib s = (case first_field "=" s of NONE => err_attribute () | SOME ("", _) => err_attribute () | SOME att => att); fun parse_chunk ["", ""] = pop | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts) | parse_chunk txts = fold (add o XML.Text) txts; -in - -fun parse_body source = - (case fold parse_chunk (split_string source) [(("", []), [])] of +fun parse_body' chunks = + (case fold parse_chunk chunks [(("", []), [])] of [(("", _), result)] => rev result | ((name, _), _) :: _ => err_unbalanced name); -fun parse source = - (case parse_body source of +fun parse' chunks = + (case parse_body' chunks of [result] => result | [] => XML.Text "" | _ => err "multiple results"); +in + +val parse_body = parse_body' o split_string; +val parse_body_bytes = parse_body' o split_bytes; + +val parse = parse' o split_string; +val parse_bytes = parse' o split_bytes; + end; val content_of = parse_body #> XML.content_of; fun is_wellformed s = string_of_body (parse_body s) = s handle Fail _ => false; end; diff --git a/src/Pure/System/options.ML b/src/Pure/System/options.ML --- a/src/Pure/System/options.ML +++ b/src/Pure/System/options.ML @@ -1,220 +1,220 @@ (* Title: Pure/System/options.ML Author: Makarius System options with external string representation. *) signature OPTIONS = sig val boolT: string val intT: string val realT: string val stringT: string val unknownT: string type T val empty: T val dest: T -> (string * Position.T) list val typ: T -> string -> string val bool: T -> string -> bool val int: T -> string -> int val real: T -> string -> real val seconds: T -> string -> Time.time val string: T -> string -> string val put_bool: string -> bool -> T -> T val put_int: string -> int -> T -> T val put_real: string -> real -> T -> T val put_string: string -> string -> T -> T val declare: {pos: Position.T, name: string, typ: string, value: string} -> T -> T val update: string -> string -> T -> T val encode: T XML.Encode.T val decode: T XML.Decode.T val default: unit -> T val default_typ: string -> string val default_bool: string -> bool val default_int: string -> int val default_real: string -> real val default_seconds: string -> Time.time val default_string: string -> string val default_put_bool: string -> bool -> unit val default_put_int: string -> int -> unit val default_put_real: string -> real -> unit val default_put_string: string -> string -> unit val get_default: string -> string val put_default: string -> string -> unit val set_default: T -> unit val reset_default: unit -> unit val load_default: unit -> unit end; structure Options: OPTIONS = struct (* representation *) val boolT = "bool"; val intT = "int"; val realT = "real"; val stringT = "string"; val unknownT = "unknown"; datatype T = Options of {pos: Position.T, typ: string, value: string} Symtab.table; val empty = Options Symtab.empty; fun dest (Options tab) = Symtab.fold (fn (name, {pos, ...}) => cons (name, pos)) tab [] |> sort_by #1; (* check *) fun check_name (Options tab) name = let val opt = Symtab.lookup tab name in if is_some opt andalso #typ (the opt) <> unknownT then the opt else error ("Unknown system option " ^ quote name) end; fun check_type options name typ = let val opt = check_name options name in if #typ opt = typ then opt else error ("Ill-typed system option " ^ quote name ^ " : " ^ #typ opt ^ " vs. " ^ typ) end; (* typ *) fun typ options name = #typ (check_name options name); (* basic operations *) fun put T print name x (options as Options tab) = let val opt = check_type options name T in Options (Symtab.update (name, {pos = #pos opt, typ = #typ opt, value = print x}) tab) end; fun get T parse options name = let val opt = check_type options name T in (case parse (#value opt) of SOME x => x | NONE => error ("Malformed value for system option " ^ quote name ^ " : " ^ T ^ " =\n" ^ quote (#value opt))) end; (* internal lookup and update *) val bool = get boolT (try Value.parse_bool); val int = get intT (try Value.parse_int); val real = get realT (try Value.parse_real); val seconds = Time.fromReal oo real; val string = get stringT SOME; val put_bool = put boolT Value.print_bool; val put_int = put intT Value.print_int; val put_real = put realT Value.print_real; val put_string = put stringT I; (* external updates *) fun check_value options name = let val opt = check_name options name in if #typ opt = boolT then ignore (bool options name) else if #typ opt = intT then ignore (int options name) else if #typ opt = realT then ignore (real options name) else if #typ opt = stringT then ignore (string options name) else () end; fun declare {pos, name, typ, value} (Options tab) = let val options' = (case Symtab.lookup tab name of SOME other => error ("Duplicate declaration of system option " ^ quote name ^ Position.here pos ^ Position.here (#pos other)) | NONE => Options (Symtab.update (name, {pos = pos, typ = typ, value = value}) tab)); val _ = typ = boolT orelse typ = intT orelse typ = realT orelse typ = stringT orelse error ("Unknown type for system option " ^ quote name ^ " : " ^ quote typ ^ Position.here pos); val _ = check_value options' name; in options' end; fun update name value (options as Options tab) = let val opt = check_name options name; val options' = Options (Symtab.update (name, {pos = #pos opt, typ = #typ opt, value = value}) tab); val _ = check_value options' name; in options' end; (* XML data *) fun encode (Options tab) = let val opts = build (tab |> Symtab.fold (fn (name, {pos, typ, value}) => cons (Position.properties_of pos, (name, (typ, value))))); open XML.Encode; in list (pair properties (pair string (pair string string))) opts end; fun decode body = let open XML.Decode; val decode_options = list (pair properties (pair string (pair string string))) #> map (fn (props, (name, (typ, value))) => {pos = Position.of_properties props, name = name, typ = typ, value = value}); in fold declare (decode_options body) empty end; (** global default **) val global_default = Synchronized.var "Options.default" (NONE: T option); fun err_no_default () = error "Missing default for system options within Isabelle process"; fun change_default f x y = Synchronized.change global_default (fn SOME options => SOME (f x y options) | NONE => err_no_default ()); fun default () = (case Synchronized.value global_default of SOME options => options | NONE => err_no_default ()); fun default_typ name = typ (default ()) name; fun default_bool name = bool (default ()) name; fun default_int name = int (default ()) name; fun default_real name = real (default ()) name; fun default_seconds name = seconds (default ()) name; fun default_string name = string (default ()) name; val default_put_bool = change_default put_bool; val default_put_int = change_default put_int; val default_put_real = change_default put_real; val default_put_string = change_default put_string; fun get_default name = let val options = default () in get (typ options name) SOME options name end; val put_default = change_default update; fun set_default options = Synchronized.change global_default (K (SOME options)); fun reset_default () = Synchronized.change global_default (K NONE); fun load_default () = (case getenv "ISABELLE_PROCESS_OPTIONS" of "" => () | name => - try File.read (Path.explode name) - |> Option.app (set_default o decode o YXML.parse_body)); + try Bytes.read (Path.explode name) + |> Option.app (set_default o decode o YXML.parse_body_bytes)); val _ = load_default (); val _ = ML_Print_Depth.set_print_depth (default_int "ML_print_depth"); end; diff --git a/src/Pure/Tools/build.ML b/src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML +++ b/src/Pure/Tools/build.ML @@ -1,120 +1,120 @@ (* Title: Pure/Tools/build.ML Author: Makarius Build Isabelle sessions. *) signature BUILD = sig type hook = string -> (theory * Document_Output.segment list) list -> unit val add_hook: hook -> unit end; structure Build: BUILD = struct (* session timing *) fun session_timing f x = let val start = Timing.start (); val y = f x; val timing = Timing.result start; val threads = string_of_int (Multithreading.max_threads ()); val props = [("threads", threads)] @ Markup.timing_properties timing; val _ = Output.protocol_message (Markup.session_timing :: props) []; in y end; (* build theories *) type hook = string -> (theory * Document_Output.segment list) list -> unit; local val hooks = Synchronized.var "Build.hooks" ([]: hook list); in fun add_hook hook = Synchronized.change hooks (cons hook); fun apply_hooks qualifier loaded_theories = Synchronized.value hooks |> List.app (fn hook => hook qualifier loaded_theories); end; fun build_theories qualifier (options, thys) = let val _ = ML_Profiling.check_mode (Options.string options "profiling"); val condition = space_explode "," (Options.string options "condition"); val conds = filter_out (can getenv_strict) condition; val loaded_theories = if null conds then (Options.set_default options; Isabelle_Process.init_options (); Future.fork I; (Thy_Info.use_theories options qualifier |> Unsynchronized.setmp print_mode (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys) else (Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^ " (undefined " ^ commas conds ^ ")\n"); []) in loaded_theories end; (* build session *) val _ = - Protocol_Command.define "build_session" + Protocol_Command.define_bytes "build_session" (fn [resources_yxml, args_yxml] => let val _ = Resources.init_session_yxml resources_yxml; val (session_name, theories) = - YXML.parse_body args_yxml |> + YXML.parse_body_bytes args_yxml |> let open XML.Decode; val position = Position.of_properties o properties; in pair string (list (pair Options.decode (list (pair string position)))) end; val _ = Session.init session_name; fun build () = let val res = theories |> (map (build_theories session_name) |> session_timing |> Exn.capture); val res1 = (case res of Exn.Res loaded_theories => Exn.capture (apply_hooks session_name) (flat loaded_theories) | Exn.Exn exn => Exn.Exn exn); val res2 = Exn.capture Session.finish (); val _ = Resources.finish_session_base (); val _ = Par_Exn.release_all [res1, res2]; val _ = if session_name = Context.PureN then Theory.install_pure (Thy_Info.get_theory Context.PureN) else (); in () end; fun exec e = if can Theory.get_pure () then Isabelle_Thread.fork {name = "build_session", stack_limit = Isabelle_Thread.stack_limit (), interrupts = false} e |> ignore else e (); in exec (fn () => (Future.interruptible_task (fn () => (build (); (0, []))) () handle exn => ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"]))) |> let open XML.Encode in pair int (list string) end |> single |> Output.protocol_message Markup.build_session_finished) end | _ => raise Match); end;