# HG changeset patch # User wenzelm # Date 1667584794 -3600 # Node ID d6d4d069770910cbea6709a2d2902ad9ffcaf8f5 # Parent 6471218877b72ccf19b64a0f4cf2dd1637143377# Parent 34a10f5dde925d68367c733a9c1d2e33492f6a96 merged diff -r 6471218877b7 -r d6d4d0697709 etc/options --- a/etc/options Fri Nov 04 13:19:52 2022 +0100 +++ b/etc/options Fri Nov 04 18:59:54 2022 +0100 @@ -178,6 +178,9 @@ option build_pide_reports : bool = true -- "report PIDE markup (in batch build)" +option pide_presentation : bool = false + -- "presentation of consolidated theories in PIDE" + section "Editor Session" @@ -226,9 +229,6 @@ option editor_syslog_limit : int = 100 -- "maximum amount of buffered syslog messages" -public option editor_presentation : bool = false - -- "dynamic presentation while editing" - section "Headless Session" diff -r 6471218877b7 -r d6d4d0697709 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Fri Nov 04 13:19:52 2022 +0100 +++ b/src/Pure/PIDE/command.ML Fri Nov 04 18:59:54 2022 +0100 @@ -26,7 +26,7 @@ type print type print_fn = Toplevel.transition -> Toplevel.state -> unit val print0: {pri: int, print_fn: print_fn} -> eval -> print - val print: bool -> (string * string list) list -> Keyword.keywords -> string -> + val print: Keyword.keywords -> bool -> (string * string list) list -> string -> eval -> print list -> print list option val parallel_print: print -> bool type print_function = @@ -362,7 +362,7 @@ make_print ("", [serial_string ()]) {delay = NONE, pri = pri, persistent = true, strict = true, print_fn = print_fn}; -fun print command_visible command_overlays keywords command_name eval old_prints = +fun print keywords visible overlays command_name eval old_prints = let val print_functions = Synchronized.value print_functions; @@ -392,8 +392,8 @@ val retained_prints = filter (fn print => print_finished print andalso print_persistent print) old_prints; val visible_prints = - if command_visible then - fold (fn (name, _) => cons (name, [])) print_functions command_overlays + if visible then + fold (fn (name, _) => cons (name, [])) print_functions overlays |> sort_distinct overlay_ord |> map_filter get_print else []; @@ -403,7 +403,7 @@ end; fun parallel_print (Print {pri, ...}) = - pri <= 0 orelse (Future.enabled () andalso Options.default_bool "parallel_print"); + pri <= 0 orelse (Future.enabled () andalso Options.default_bool \<^system_option>\parallel_print\); fun print_function name f = Synchronized.change print_functions (fn funs => @@ -497,7 +497,8 @@ val _ = Command.print_function "print_state" (fn {keywords, command_name, ...} => - if Options.default_bool "editor_output_state" andalso Keyword.is_printed keywords command_name + if Options.default_bool \<^system_option>\editor_output_state\ + andalso Keyword.is_printed keywords command_name then SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false, print_fn = fn _ => fn st => diff -r 6471218877b7 -r d6d4d0697709 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri Nov 04 13:19:52 2022 +0100 +++ b/src/Pure/PIDE/document.ML Fri Nov 04 18:59:54 2022 +0100 @@ -125,20 +125,18 @@ fun read_header node span = let - val {header, errors, ...} = get_header node; - val _ = - if null errors then () - else - cat_lines errors |> - (case Position.id_of (Position.thread_data ()) of - NONE => I - | SOME id => Protocol_Message.command_positions_yxml id) - |> error; - val {name = (name, _), imports, ...} = header; - val {name = (_, pos), imports = imports', keywords} = - Thy_Header.read_tokens Position.none span; - val imports'' = (map #1 imports ~~ map #2 imports') handle ListPair.UnequalLengths => imports; - in Thy_Header.make (name, pos) imports'' keywords end; + val (name, imports0) = + (case get_header node of + {errors = [], header = {name = (name, _), imports, ...}, ...} => (name, imports) + | {errors, ...} => + cat_lines errors |> + (case Position.id_of (Position.thread_data ()) of + NONE => I + | SOME id => Protocol_Message.command_positions_yxml id) + |> error); + val {name = (_, pos), imports = imports1, keywords} = Thy_Header.read_tokens Position.none span; + val imports = (map #1 imports0 ~~ map #2 imports1) handle ListPair.UnequalLengths => imports0; + in Thy_Header.make (name, pos) imports keywords end; fun get_perspective (Node {perspective, ...}) = perspective; @@ -147,10 +145,10 @@ (header, keywords, make_perspective args, entries, result, consolidated)); val required_node = #required o get_perspective; -val visible_command = Inttab.defined o #visible o get_perspective; +val command_overlays = Inttab.lookup_list o #overlays o get_perspective; +val command_visible = Inttab.defined o #visible o get_perspective; val visible_last = #visible_last o get_perspective; val visible_node = is_some o visible_last -val overlays = Inttab.lookup_list o #overlays o get_perspective; fun map_entries f = map_node (fn (header, keywords, perspective, entries, result, consolidated) => @@ -472,8 +470,6 @@ NONE => err_undef "command" command_id | SOME command => command); -val the_command_name = #1 oo the_command; - (* execution *) @@ -534,7 +530,7 @@ let val {version_id, execution_id, delay_request, parallel_prints} = execution; - val delay = seconds (Options.default_real "editor_execution_delay"); + val delay = seconds (Options.default_real \<^system_option>\editor_execution_delay\); val _ = Future.cancel delay_request; val delay_request' = Event_Timer.future {physical = true} (Time.now () + delay); @@ -595,7 +591,7 @@ fun assign_update_change entry (tab: assign_update) : assign_update = Inttab.update entry tab; fun assign_update_apply (tab: assign_update) node = Inttab.fold assign_entry tab node; -fun assign_update_new upd (tab: assign_update) = +fun assign_update_new upd (tab: assign_update) : assign_update = Inttab.update_new upd tab handle Inttab.DUP dup => err_dup "exec state assignment" dup; @@ -638,15 +634,14 @@ val _ = Output.status [Markup.markup_only Markup.initialized]; in thy end; -fun check_root_theory node = +fun get_special_parent node = let val master_dir = master_directory node; - val header = #header (get_header node); - val header_name = #1 (#name header); + val header as {name = (name, _), ...} = #header (get_header node); val parent = - if header_name = Sessions.root_name then + if name = Sessions.root_name then SOME (Thy_Info.get_theory Sessions.theory_name) - else if member (op =) Thy_Header.ml_roots header_name then + else if member (op =) Thy_Header.ml_roots name then SOME (Thy_Info.get_theory Thy_Header.ml_bootstrapN) else NONE; in parent |> Option.map (fn thy => Resources.begin_theory master_dir header [thy]) end; @@ -655,7 +650,7 @@ Thy_Info.defined_theory name orelse null (#errors (get_header node)) andalso (not full orelse is_some (get_result node)); -fun last_common keywords state node_required node0 node = +fun last_common keywords the_command_name node_required node0 node = let fun update_flags prev (visible, initial) = let @@ -663,7 +658,7 @@ val initial' = initial andalso (case prev of NONE => true - | SOME command_id => the_command_name state command_id <> Thy_Header.theoryN); + | SOME command_id => the_command_name command_id <> Thy_Header.theoryN); in (visible', initial') end; fun get_common ((prev, command_id), opt_exec) (_, ok, flags, assign_update) = @@ -680,13 +675,11 @@ (case opt_exec of SOME (eval, prints) => let - val command_visible = visible_command node command_id; - val command_overlays = overlays node command_id; - val command_name = the_command_name state command_id; - val command_print = - Command.print command_visible command_overlays keywords command_name eval prints; + val visible = command_visible node command_id; + val overlays = command_overlays node command_id; + val command_name = the_command_name command_id; in - (case command_print of + (case Command.print keywords visible overlays command_name eval prints of SOME prints' => assign_update_new (command_id, SOME (eval, prints')) | NONE => I) end @@ -708,8 +701,8 @@ if not proper_init andalso is_none init then NONE else let - val command_visible = visible_command node command_id'; - val command_overlays = overlays node command_id'; + val visible = command_visible node command_id'; + val overlays = command_overlays node command_id'; val (command_name, blob_digests, blobs_index, span0) = the_command state command_id'; val blobs = map (resolve_blob state) blob_digests; val span = Lazy.force span0; @@ -717,8 +710,7 @@ val eval' = Command.eval keywords (master_directory node) (fn () => the_default illegal_init init span) (blobs, blobs_index) command_id' span (#1 (#2 command_exec)); - val prints' = - perhaps (Command.print command_visible command_overlays keywords command_name eval') []; + val prints' = perhaps (Command.print keywords visible overlays command_name eval') []; val exec' = (eval', prints'); val assign_update' = assign_update_new (command_id', SOME exec') assign_update; @@ -728,95 +720,100 @@ fun removed_execs node0 (command_id, exec_ids) = subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id)); -fun print_consolidation options the_command_span node_name (assign_update, node) = - (case finished_result_theory node of - SOME (result_id, thy) => - timeit "Document.print_consolidation" (fn () => - let - val active_tasks = - (node, false) |-> iterate_entries (fn (_, opt_exec) => fn active => - if active then NONE - else - (case opt_exec of - NONE => NONE - | SOME (eval, _) => - SOME (not (null (Execution.snapshot [Command.eval_exec_id eval]))))); - in - if not active_tasks then - let - fun commit_consolidated () = - (Lazy.force (get_consolidated node); - Output.status [Markup.markup_only Markup.consolidated]); - val consolidation = - if Options.bool options "editor_presentation" then - let - val (_, offsets, rev_segments) = - iterate_entries (fn ((prev, _), opt_exec) => fn (offset, offsets, segments) => - (case opt_exec of - SOME (eval, _) => - let - val command_id = Command.eval_command_id eval; - val span = the_command_span command_id; +fun finished_eval node = + let + val active = + (node, false) |-> iterate_entries (fn (_, opt_exec) => fn active => + if active then NONE + else + (case opt_exec of + NONE => SOME true + | SOME (eval, _) => SOME (not (null (Execution.snapshot [Command.eval_exec_id eval]))))); + in not active end; - val st = - (case try (#1 o the o the_entry node o the) prev of - NONE => Toplevel.make_state NONE - | SOME prev_eval => Command.eval_result_state prev_eval); +fun presentation_context options the_command_span node_name node : Thy_Info.presentation_context = + let + val (_, offsets, rev_segments) = + (node, (0, Inttab.empty, [])) |-> iterate_entries + (fn ((prev, id), opt_exec) => fn (offset, offsets, segments) => + (case opt_exec of + SOME (eval, _) => + let + val command_id = Command.eval_command_id eval; + val span = the_command_span command_id; - val exec_id = Command.eval_exec_id eval; - val tr = Command.eval_result_command eval; - val st' = Command.eval_result_state eval; + val st = + (case try (#1 o the o the_entry node o the) prev of + NONE => Toplevel.make_state NONE + | SOME prev_eval => Command.eval_result_state prev_eval); + + val exec_id = Command.eval_exec_id eval; + val tr = Command.eval_result_command eval; + val st' = Command.eval_result_state eval; + + val offset' = offset + the_default 0 (Command_Span.symbol_length span); + val offsets' = offsets + |> Inttab.update (command_id, offset) + |> Inttab.update (exec_id, offset); + val segments' = (span, (st, tr, st')) :: segments; + in SOME (offset', offsets', segments') end + | NONE => raise Fail ("Unassigned exec " ^ Value.print_int id))); - val offset' = offset + the_default 0 (Command_Span.symbol_length span); - val offsets' = offsets - |> Inttab.update (command_id, offset) - |> Inttab.update (exec_id, offset); - val segments' = (span, (st, tr, st')) :: segments; - in SOME (offset', offsets', segments') end - | NONE => NONE)) node (0, Inttab.empty, []); - - val adjust = Inttab.lookup offsets; - val segments = - rev rev_segments |> map (fn (span, (st, tr, st')) => - {span = Command_Span.adjust_offsets adjust span, - prev_state = st, command = tr, state = st'}); + val adjust = Inttab.lookup offsets; + val segments = + rev rev_segments |> map (fn (span, (st, tr, st')) => + {span = Command_Span.adjust_offsets adjust span, + prev_state = st, command = tr, state = st'}); + in + {options = options, + file_pos = Position.file node_name, + adjust_pos = Position.adjust_offsets adjust, + segments = segments} + end; - val presentation_context: Thy_Info.presentation_context = - {options = options, - file_pos = Position.file node_name, - adjust_pos = Position.adjust_offsets adjust, - segments = segments}; - in - fn _ => - let - val _ = Output.status [Markup.markup_only Markup.consolidating]; - val res = Exn.capture (Thy_Info.apply_presentation presentation_context) thy; - val _ = commit_consolidated (); - in Exn.release res end - end - else fn _ => commit_consolidated (); +fun print_consolidation options the_command_span node_name (assign_update, node) = + timeit "Document.print_consolidation" (fn () => + (case finished_result_theory node of + SOME (result_id, thy) => + if finished_eval node then + let + fun commit_consolidated () = + (Lazy.force (get_consolidated node); + Output.status [Markup.markup_only Markup.consolidated]); + val consolidation = + if Options.bool options \<^system_option>\pide_presentation\ then + let val context = presentation_context options the_command_span node_name node in + fn _ => + let + val _ = Output.status [Markup.markup_only Markup.consolidating]; + val res = Exn.capture (Thy_Info.apply_presentation context) thy; + val _ = commit_consolidated (); + in Exn.release res end + end + else fn _ => commit_consolidated (); - val result_entry = - (case lookup_entry node result_id of - NONE => err_undef "result command entry" result_id - | SOME (eval, prints) => - let - val print = eval |> Command.print0 - {pri = Task_Queue.urgent_pri + 1, print_fn = K consolidation}; - in (result_id, SOME (eval, print :: prints)) end); + val result_entry = + (case lookup_entry node result_id of + NONE => err_undef "result command entry" result_id + | SOME (eval, prints) => + let + val print = eval |> Command.print0 + {pri = Task_Queue.urgent_pri + 1, print_fn = K consolidation}; + in (result_id, SOME (eval, print :: prints)) end); - val assign_update' = assign_update |> assign_update_change result_entry; - val node' = node |> assign_entry result_entry; - in (assign_update', node') end - else (assign_update, node) - end) - | NONE => (assign_update, node)); + val assign_update' = assign_update |> assign_update_change result_entry; + val node' = node |> assign_entry result_entry; + in (assign_update', node') end + else (assign_update, node) + | NONE => (assign_update, node))); + in fun update old_version_id new_version_id edits consolidate state = Runtime.exn_trace_system (fn () => let val options = Options.default (); + val the_command_name = #1 o the_command state; val the_command_span = Outer_Syntax.make_span o Lazy.force o #4 o the_command state; val old_version = the_version state old_version_id; @@ -828,7 +825,7 @@ val nodes = nodes_of new_version; val required = make_required nodes; val required0 = make_required (nodes_of old_version); - val edited = Symtab.build (edits |> fold (fn (name, _) => Symtab.update (name, ()))); + val edited = Symtab.build (edits |> fold (Symtab.insert_set o #1)); val updated = timeit "Document.update" (fn () => nodes |> String_Graph.schedule @@ -840,7 +837,7 @@ timeit ("Document.update " ^ name) (fn () => Runtime.exn_trace_system (fn () => let - val root_theory = check_root_theory node; + val special_parent = get_special_parent node; val keywords = node_keywords name node; val maybe_consolidate = consolidate name andalso could_consolidate node; @@ -856,19 +853,19 @@ val node0 = node_of old_version name; val init = init_theory imports node; val proper_init = - is_some root_theory orelse + is_some special_parent orelse check_theory false name node andalso forall (fn (name, (_, node)) => check_theory true name node) imports; val (print_execs, common, (still_visible, initial)) = if imports_result_changed then (assign_update_empty, NONE, (true, true)) - else last_common keywords state node_required node0 node; + else last_common keywords the_command_name node_required node0 node; val common_command_exec = (case common of SOME id => (id, the_default Command.no_exec (the_entry node id)) - | NONE => (Document_ID.none, Command.init_exec root_theory)); + | NONE => (Document_ID.none, Command.init_exec special_parent)); val (updated_execs, (command_id', exec'), _) = (print_execs, common_command_exec, if initial then SOME init else NONE) diff -r 6471218877b7 -r d6d4d0697709 src/Pure/Thy/document_output.ML --- a/src/Pure/Thy/document_output.ML Fri Nov 04 13:19:52 2022 +0100 +++ b/src/Pure/Thy/document_output.ML Fri Nov 04 18:59:54 2022 +0100 @@ -16,7 +16,7 @@ type segment = {span: Command_Span.span, command: Toplevel.transition, prev_state: Toplevel.state, state: Toplevel.state} - val present_thy: Options.T -> Keyword.keywords -> segment list -> Latex.text + val present_thy: Options.T -> Keyword.keywords -> string -> segment list -> Latex.text val pretty_term: Proof.context -> term -> Pretty.T val pretty_thm: Proof.context -> thm -> Pretty.T val isabelle: Proof.context -> Latex.text -> Latex.text @@ -400,7 +400,7 @@ in -fun present_thy options keywords (segments: segment list) = +fun present_thy options keywords thy_name (segments: segment list) = let (* tokens *) @@ -479,6 +479,7 @@ |> present (Toplevel.make_state NONE) (spans ~~ command_results) |> present_trailer |> rev + |> Latex.isabelle_body thy_name else error "Messed-up outer syntax for presentation" end; diff -r 6471218877b7 -r d6d4d0697709 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Fri Nov 04 13:19:52 2022 +0100 +++ b/src/Pure/Thy/thy_info.ML Fri Nov 04 18:59:54 2022 +0100 @@ -59,14 +59,12 @@ if exists (Toplevel.is_skipped_proof o #state) segments then () else let - val body = Document_Output.present_thy options (Thy_Header.get_keywords thy) segments; + val keywords = Thy_Header.get_keywords thy; + val thy_name = Context.theory_name thy; + val latex = Document_Output.present_thy options keywords thy_name segments; in if Options.string options "document" = "false" then () - else - let - val thy_name = Context.theory_name thy; - val latex = Latex.isabelle_body thy_name body; - in Export.export thy \<^path_binding>\document/latex\ latex end + else Export.export thy \<^path_binding>\document/latex\ latex end)); diff -r 6471218877b7 -r d6d4d0697709 src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Fri Nov 04 13:19:52 2022 +0100 +++ b/src/Pure/Tools/dump.scala Fri Nov 04 18:59:54 2022 +0100 @@ -102,8 +102,8 @@ options0 + "parallel_proofs=0" + "completion_limit=0" + - "editor_tracing_messages=0" + - "editor_presentation" + "pide_presentation" + + "editor_tracing_messages=0" aspects.foldLeft(options1) { case (opts, aspect) => aspect.options.foldLeft(opts)(_ + _) } }