# HG changeset patch # User nipkow # Date 1667564392 -3600 # Node ID 6471218877b72ccf19b64a0f4cf2dd1637143377 # Parent e800cc580c80f8b0e14a650972b94dd3a81b8d92# Parent 2612b3406b61242f34d225e012f0d2cc071996d6 merged diff -r 2612b3406b61 -r 6471218877b7 src/Doc/Demo_Easychair/ROOT --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Demo_Easychair/ROOT Fri Nov 04 13:19:52 2022 +0100 @@ -0,0 +1,9 @@ +session Demo_Easychair (doc) = HOL + + options [document_variants = "demo_easychair"] + theories + Document + document_files (in "$ISABELLE_EASYCHAIR_HOME") + "easychair.cls" + document_files + "root.bib" + "root.tex" diff -r 2612b3406b61 -r 6471218877b7 src/Doc/Demo_FoilTeX/ROOT --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Demo_FoilTeX/ROOT Fri Nov 04 13:19:52 2022 +0100 @@ -0,0 +1,11 @@ +session Demo_FoilTeX (doc) = HOL + + options [document_variants = "demo_foiltex", + document_build = "pdflatex", document_logo = "FoilTeX"] + theories + Document + document_files (in "$ISABELLE_FOILTEX_HOME") + "fltfonts.def" + "foil20.clo" + "foils.cls" + document_files + "root.tex" diff -r 2612b3406b61 -r 6471218877b7 src/Doc/Demo_LIPIcs/ROOT --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Demo_LIPIcs/ROOT Fri Nov 04 13:19:52 2022 +0100 @@ -0,0 +1,12 @@ +session Demo_LIPIcs (doc) = HOL + + options [document_variants = "demo_lipics", + document_build = "pdflatex", document_heading_prefix = "", document_comment_latex] + theories + Document + document_files (in "$ISABELLE_LIPICS_HOME") + "cc-by.pdf" + "lipics-logo-bw.pdf" + "lipics-v2021.cls" + document_files + "root.bib" + "root.tex" diff -r 2612b3406b61 -r 6471218877b7 src/Doc/ROOT --- a/src/Doc/ROOT Thu Nov 03 14:20:07 2022 +0100 +++ b/src/Doc/ROOT Fri Nov 04 13:19:52 2022 +0100 @@ -488,38 +488,3 @@ document_files "root.tex" "style.sty" - -session Demo_Easychair (doc) in "Demo_Easychair" = HOL + - options [document_variants = "demo_easychair"] - theories - Document - document_files (in "$ISABELLE_EASYCHAIR_HOME") - "easychair.cls" - document_files - "root.bib" - "root.tex" - -session Demo_FoilTeX (doc) in "Demo_FoilTeX" = HOL + - options [document_variants = "demo_foiltex", - document_build = "pdflatex", document_logo = "FoilTeX"] - theories - Document - document_files (in "$ISABELLE_FOILTEX_HOME") - "fltfonts.def" - "foil20.clo" - "foils.cls" - document_files - "root.tex" - -session Demo_LIPIcs (doc) in "Demo_LIPIcs" = HOL + - options [document_variants = "demo_lipics", - document_build = "pdflatex", document_heading_prefix = "", document_comment_latex] - theories - Document - document_files (in "$ISABELLE_LIPICS_HOME") - "cc-by.pdf" - "lipics-logo-bw.pdf" - "lipics-v2021.cls" - document_files - "root.bib" - "root.tex" diff -r 2612b3406b61 -r 6471218877b7 src/Doc/ROOTS --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/ROOTS Fri Nov 04 13:19:52 2022 +0100 @@ -0,0 +1,3 @@ +Demo_Easychair +Demo_FoilTeX +Demo_LIPIcs diff -r 2612b3406b61 -r 6471218877b7 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Thu Nov 03 14:20:07 2022 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Fri Nov 04 13:19:52 2022 +0100 @@ -195,7 +195,7 @@ fun diag_state ctxt = (case Diag_State.get ctxt of SOME st => st - | NONE => Toplevel.init_toplevel ()); + | NONE => Toplevel.make_state NONE); val diag_goal = Proof.goal o Toplevel.proof_of o diag_state; diff -r 2612b3406b61 -r 6471218877b7 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Thu Nov 03 14:20:07 2022 +0100 +++ b/src/Pure/Isar/toplevel.ML Fri Nov 04 13:19:52 2022 +0100 @@ -8,8 +8,7 @@ sig exception UNDEF type state - val init_toplevel: unit -> state - val theory_toplevel: theory -> state + val make_state: theory option -> state val is_toplevel: state -> bool val is_theory: state -> bool val is_proof: state -> bool @@ -149,8 +148,9 @@ fun previous_theory_of (State (_, (prev_thy, _))) = prev_thy; fun output_of (State (_, (_, output))) = output; -fun init_toplevel () = State (node_presentation Toplevel, (NONE, NONE)); -fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), (NONE, NONE)); +fun make_state opt_thy = + let val node = (case opt_thy of NONE => Toplevel | SOME thy => Theory (Context.Theory thy)) + in State (node_presentation node, (NONE, NONE)) end; fun level state = (case node_of state of @@ -270,7 +270,7 @@ Init of unit -> theory | (*formal exit of theory*) Exit | - (*peek at state*) + (*keep state unchanged*) Keep of bool -> presentation | (*node transaction and presentation*) Transaction of (bool -> node -> node_presentation) * presentation; @@ -717,7 +717,7 @@ let fun add (tr, st') res = (case res of - [] => [(init_toplevel (), tr, st')] + [] => [(make_state NONE, tr, st')] | (_, _, st) :: _ => (st, tr, st') :: res); fun acc (Result r) = add r | acc (Result_List rs) = fold acc rs diff -r 2612b3406b61 -r 6471218877b7 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Thu Nov 03 14:20:07 2022 +0100 +++ b/src/Pure/PIDE/command.ML Fri Nov 04 13:19:52 2022 +0100 @@ -170,10 +170,7 @@ fun init_eval_state opt_thy = {failed = false, command = Toplevel.empty, - state = - (case opt_thy of - NONE => Toplevel.init_toplevel () - | SOME thy => Toplevel.theory_toplevel thy)}; + state = Toplevel.make_state opt_thy}; datatype eval = Eval of @@ -312,6 +309,7 @@ fun print_exec_id (Print {exec_id, ...}) = exec_id; val print_eq = op = o apply2 print_exec_id; +fun print_equiv (name', args') (Print {name, args, ...}) = name' = name andalso args' = args; type print_fn = Toplevel.transition -> Toplevel.state -> unit; @@ -383,7 +381,7 @@ end; fun get_print (name, args) = - (case find_first (fn Print print => (#name print, #args print) = (name, args)) old_prints of + (case find_first (print_equiv (name, args)) old_prints of NONE => (case AList.lookup (op =) print_functions name of NONE => @@ -409,9 +407,10 @@ fun print_function name f = Synchronized.change print_functions (fn funs => - (if name = "" then error "Unnamed print function" else (); - if not (AList.defined (op =) funs name) then () - else warning ("Redefining command print function: " ^ quote name); + (if name = "" then error "Unnamed print function" + else if AList.defined (op =) funs name then + warning ("Redefining command print function: " ^ quote name) + else (); AList.update (op =) (name, f) funs)); fun no_print_function name = @@ -419,25 +418,6 @@ end; -val _ = - print_function "Execution.print" - (fn {args, exec_id, ...} => - if null args then - SOME {delay = NONE, pri = Task_Queue.urgent_pri + 2, persistent = false, strict = false, - print_fn = fn _ => fn _ => Execution.fork_prints exec_id} - else NONE); - -val _ = - print_function "print_state" - (fn {keywords, command_name, ...} => - if Options.default_bool "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 => - if Toplevel.is_proof st then Output.state (Toplevel.string_of_state st) - else ()} - else NONE); - (* combined execution *) @@ -502,3 +482,25 @@ end; end; + + +(* common print functions *) + +val _ = + Command.print_function "Execution.print" + (fn {args, exec_id, ...} => + if null args then + SOME {delay = NONE, pri = Task_Queue.urgent_pri + 2, persistent = false, strict = false, + print_fn = fn _ => fn _ => Execution.fork_prints exec_id} + else NONE); + +val _ = + Command.print_function "print_state" + (fn {keywords, command_name, ...} => + if Options.default_bool "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 => + if Toplevel.is_proof st then Output.state (Toplevel.string_of_state st) + else ()} + else NONE); diff -r 2612b3406b61 -r 6471218877b7 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu Nov 03 14:20:07 2022 +0100 +++ b/src/Pure/PIDE/document.ML Fri Nov 04 13:19:52 2022 +0100 @@ -123,8 +123,6 @@ map_node (fn (header, _, perspective, entries, result, consolidated) => (header, keywords, perspective, entries, result, consolidated)); -fun get_keywords (Node {keywords, ...}) = keywords; - fun read_header node span = let val {header, errors, ...} = get_header node; @@ -190,17 +188,15 @@ in SOME (result_id, Toplevel.end_theory Position.none st) handle ERROR _ => NONE end else NONE; +fun get_consolidated (Node {consolidated, ...}) = consolidated; + val reset_consolidated = map_node (fn (header, keywords, perspective, entries, result, _) => (header, keywords, perspective, entries, result, Lazy.lazy I)); -fun commit_consolidated (Node {consolidated, ...}) = - (Lazy.force consolidated; Output.status [Markup.markup_only Markup.consolidated]); - -fun consolidated_node (Node {consolidated, ...}) = Lazy.is_finished consolidated; - fun could_consolidate node = - not (consolidated_node node) andalso is_some (finished_result_theory node); + not (Lazy.is_finished (get_consolidated node)) andalso + is_some (finished_result_theory node); fun get_node nodes name = String_Graph.get_node nodes name handle String_Graph.UNDEF _ => empty_node; @@ -208,6 +204,21 @@ fun update_node name f = default_node name #> String_Graph.map_node name f; +(* outer syntax keywords *) + +val pure_keywords = Thy_Header.get_keywords o Theory.get_pure; + +fun theory_keywords name = + (case Thy_Info.lookup_theory name of + SOME thy => Thy_Header.get_keywords thy + | NONE => Keyword.empty_keywords); + +fun node_keywords name node = + (case node of + Node {keywords = SOME keywords, ...} => keywords + | _ => theory_keywords name); + + (* node edits and associated executions *) type overlay = Document_ID.command * (string * string list); @@ -279,9 +290,8 @@ else let val {master, header, errors} = get_header node; - val imports_keywords = map_filter (get_keywords o get_node nodes o #1) (#imports header); - val keywords = - Library.foldl Keyword.merge_keywords (Session.get_keywords (), imports_keywords); + val imports_keywords = map (node_keywords name o get_node nodes o #1) (#imports header); + val keywords = Library.foldl Keyword.merge_keywords (pure_keywords (), imports_keywords); val (keywords', errors') = (Keyword.add_keywords (#keywords header) keywords, errors) handle ERROR msg => @@ -534,7 +544,7 @@ |> map_filter (Command.exec_parallel_prints execution_id [delay]); fun finished_import (name, (node, _)) = - finished_result node orelse is_some (Thy_Info.lookup_theory name); + finished_result node orelse Thy_Info.defined_theory name; val nodes = nodes_of (the_version state version_id); val required = make_required nodes; @@ -582,7 +592,7 @@ val assign_update_empty: assign_update = Inttab.empty; fun assign_update_defined (tab: assign_update) command_id = Inttab.defined tab command_id; -fun assign_update_change entry (tab: assign_update) = Inttab.update entry tab; +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) = @@ -604,7 +614,7 @@ val imports = #imports header; fun maybe_eval_result eval = Command.eval_result_state eval - handle Fail _ => Toplevel.init_toplevel (); + handle Fail _ => Toplevel.make_state NONE; fun maybe_end_theory pos st = SOME (Toplevel.end_theory pos st) handle ERROR msg => (Output.error_message msg; NONE); @@ -615,7 +625,7 @@ NONE => maybe_end_theory pos (case get_result (snd (the (AList.lookup (op =) deps import))) of - NONE => Toplevel.init_toplevel () + NONE => Toplevel.make_state NONE | SOME (_, eval) => maybe_eval_result eval) |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))) | SOME thy => SOME (thy, (Position.none, Markup.empty)))); @@ -642,7 +652,7 @@ in parent |> Option.map (fn thy => Resources.begin_theory master_dir header [thy]) end; fun check_theory full name node = - is_some (Thy_Info.lookup_theory name) orelse + 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 = @@ -673,10 +683,10 @@ 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; in - (case - Command.print command_visible command_overlays keywords command_name eval prints - of + (case command_print of SOME prints' => assign_update_new (command_id, SOME (eval, prints')) | NONE => I) end @@ -721,81 +731,85 @@ fun print_consolidation options the_command_span node_name (assign_update, node) = (case finished_result_theory node of SOME (result_id, thy) => - 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 - 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; + 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; - val st = - (case try (#1 o the o the_entry node o the) prev of - NONE => Toplevel.init_toplevel () - | SOME prev_eval => Command.eval_result_state prev_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 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 => NONE)) node (0, Inttab.empty, []); + 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'}); + 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 (); - 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 _ => + val result_entry = + (case lookup_entry node result_id of + NONE => err_undef "result command entry" result_id + | SOME (eval, prints) => let - val _ = Output.status [Markup.markup_only Markup.consolidating]; - val res = Exn.capture (Thy_Info.apply_presentation presentation_context) thy; - val _ = commit_consolidated node; - in Exn.release res end - end - else fn _ => commit_consolidated node; + 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 + 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)); in @@ -827,7 +841,7 @@ Runtime.exn_trace_system (fn () => let val root_theory = check_root_theory node; - val keywords = the_default (Session.get_keywords ()) (get_keywords node); + val keywords = node_keywords name node; val maybe_consolidate = consolidate name andalso could_consolidate node; val imports = map (apsnd Future.join) deps; diff -r 2612b3406b61 -r 6471218877b7 src/Pure/PIDE/query_operation.ML --- a/src/Pure/PIDE/query_operation.ML Thu Nov 03 14:20:07 2022 +0100 +++ b/src/Pure/PIDE/query_operation.ML Fri Nov 04 13:19:52 2022 +0100 @@ -39,14 +39,13 @@ in () end)} | _ => NONE); +end; (* print_state *) val _ = - register {name = "print_state", pri = Task_Queue.urgent_pri} + Query_Operation.register {name = "print_state", pri = Task_Queue.urgent_pri} (fn {state = st, output_result, ...} => if Toplevel.is_proof st then output_result (Markup.markup Markup.state (Toplevel.string_of_state st)) else ()); - -end; diff -r 2612b3406b61 -r 6471218877b7 src/Pure/PIDE/session.ML --- a/src/Pure/PIDE/session.ML Thu Nov 03 14:20:07 2022 +0100 +++ b/src/Pure/PIDE/session.ML Fri Nov 04 13:19:52 2022 +0100 @@ -9,7 +9,6 @@ val init: string -> unit val get_name: unit -> string val welcome: unit -> string - val get_keywords: unit -> Keyword.keywords val shutdown: unit -> unit val finish: unit -> unit end; @@ -30,18 +29,6 @@ fun welcome () = "Welcome to " ^ description () ^ Isabelle_System.isabelle_heading (); -(* base syntax *) - -val keywords = Synchronized.var "Session.keywords" Keyword.empty_keywords; - -fun get_keywords () = Synchronized.value keywords; - -fun update_keywords () = - Synchronized.change keywords - (K (fold (curry Keyword.merge_keywords o Thy_Header.get_keywords o Thy_Info.get_theory) - (Thy_Info.get_names ()) Keyword.empty_keywords)); - - (* finish *) fun shutdown () = @@ -53,7 +40,6 @@ (shutdown (); Par_List.map (Global_Theory.get_thm_names o Thy_Info.get_theory) (Thy_Info.get_names ()); Thy_Info.finish (); - shutdown (); - update_keywords ()); + shutdown ()); end; diff -r 2612b3406b61 -r 6471218877b7 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Thu Nov 03 14:20:07 2022 +0100 +++ b/src/Pure/PIDE/session.scala Fri Nov 04 13:19:52 2022 +0100 @@ -367,7 +367,7 @@ /* manager thread */ - private val delay_prune = + private lazy val delay_prune = Delay.first(prune_delay) { manager.send(Prune_History) } private val manager: Consumer_Thread[Any] = { diff -r 2612b3406b61 -r 6471218877b7 src/Pure/Thy/document_output.ML --- a/src/Pure/Thy/document_output.ML Thu Nov 03 14:20:07 2022 +0100 +++ b/src/Pure/Thy/document_output.ML Fri Nov 04 13:19:52 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 -> theory -> segment list -> Latex.text + val present_thy: Options.T -> Keyword.keywords -> 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 @@ -293,21 +293,20 @@ val document_tags_default = map_filter #1 document_tags; val document_tags_command = map_filter #2 document_tags; in - fn cmd_name => fn state => fn state' => fn active_tag => + fn name => fn st => fn st' => fn active_tag => let val keyword_tags = - if cmd_name = "end" andalso Toplevel.is_end_theory state' then ["theory"] - else Keyword.command_tags keywords cmd_name; + if Keyword.is_theory_end keywords name andalso Toplevel.is_end_theory st' then ["theory"] + else Keyword.command_tags keywords name; val command_tags = - the_list (AList.lookup (op =) document_tags_command cmd_name) @ + the_list (AList.lookup (op =) document_tags_command name) @ keyword_tags @ document_tags_default; val active_tag' = (case command_tags of default_tag :: _ => SOME default_tag | [] => - if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state - then active_tag - else NONE); + if Keyword.is_vacuous keywords name andalso Toplevel.is_proof st + then active_tag else NONE); in active_tag' end end; @@ -401,11 +400,8 @@ in -fun present_thy options thy (segments: segment list) = +fun present_thy options keywords (segments: segment list) = let - val keywords = Thy_Header.get_keywords thy; - - (* tokens *) val ignored = Scan.state --| ignore @@ -480,7 +476,7 @@ in if length command_results = length spans then (([], []), NONE, true, [], (I, I)) - |> present (Toplevel.init_toplevel ()) (spans ~~ command_results) + |> present (Toplevel.make_state NONE) (spans ~~ command_results) |> present_trailer |> rev else error "Messed-up outer syntax for presentation" diff -r 2612b3406b61 -r 6471218877b7 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Thu Nov 03 14:20:07 2022 +0100 +++ b/src/Pure/Thy/thy_info.ML Fri Nov 04 13:19:52 2022 +0100 @@ -15,6 +15,7 @@ val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory val get_names: unit -> string list val lookup_theory: string -> theory option + val defined_theory: string -> bool val get_theory: string -> theory val master_directory: string -> Path.T val remove_thy: string -> unit @@ -58,7 +59,7 @@ if exists (Toplevel.is_skipped_proof o #state) segments then () else let - val body = Document_Output.present_thy options thy segments; + val body = Document_Output.present_thy options (Thy_Header.get_keywords thy) segments; in if Options.string options "document" = "false" then () else @@ -138,6 +139,8 @@ SOME (_, SOME theory) => SOME theory | _ => NONE); +val defined_theory = is_some o lookup_theory; + fun get_theory name = (case lookup_theory name of SOME theory => theory @@ -289,7 +292,7 @@ in (results, (st', pos')) end; val (results, (end_state, end_pos)) = - fold_map element_result elements (Toplevel.init_toplevel (), Position.none); + fold_map element_result elements (Toplevel.make_state NONE, Position.none); val thy = Toplevel.end_theory end_pos end_state; in (results, thy) end; @@ -431,7 +434,7 @@ let val trs = Outer_Syntax.parse_text thy (K thy) pos txt; val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs); - val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ()); + val end_state = fold (Toplevel.command_exception true) trs (Toplevel.make_state NONE); in Toplevel.end_theory end_pos end_state end; diff -r 2612b3406b61 -r 6471218877b7 src/Pure/Tools/print_operation.ML --- a/src/Pure/Tools/print_operation.ML Thu Nov 03 14:20:07 2022 +0100 +++ b/src/Pure/Tools/print_operation.ML Fri Nov 04 13:19:52 2022 +0100 @@ -52,22 +52,23 @@ end; +end; + (* common print operations *) val _ = - register "context" "context of local theory target" Toplevel.pretty_context; + Print_Operation.register "context" "context of local theory target" + Toplevel.pretty_context; val _ = - register "cases" "cases of proof context" + Print_Operation.register "cases" "cases of proof context" (Proof_Context.pretty_cases o Toplevel.context_of); val _ = - register "terms" "term bindings of proof context" + Print_Operation.register "terms" "term bindings of proof context" (Proof_Context.pretty_term_bindings o Toplevel.context_of); val _ = - register "theorems" "theorems of local theory or proof context" + Print_Operation.register "theorems" "theorems of local theory or proof context" (Isar_Cmd.pretty_theorems false); - -end; diff -r 2612b3406b61 -r 6471218877b7 src/ZF/WF.thy --- a/src/ZF/WF.thy Thu Nov 03 14:20:07 2022 +0100 +++ b/src/ZF/WF.thy Fri Nov 04 13:19:52 2022 +0100 @@ -361,12 +361,11 @@ wfrec[A](r,a,H) = H(a, \x\(r-``{a}) \ A. wfrec[A](r,x,H))" unfolding wf_on_def wfrec_on_def apply (erule wfrec [THEN trans]) -apply (simp add: vimage_Int_square cons_subset_iff) +apply (simp add: vimage_Int_square) done text\Minimal-element characterization of well-foundedness\ -lemma wf_eq_minimal: - "wf(r) \ (\Q x. x \ Q \ (\z\Q. \y. \y,z\:r \ y\Q))" -by (unfold wf_def, blast) +lemma wf_eq_minimal: "wf(r) \ (\Q x. x \ Q \ (\z\Q. \y. \y,z\:r \ y\Q))" + unfolding wf_def by blast end