--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Demo_Easychair/ROOT Thu Nov 03 21:09:37 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"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Demo_FoilTeX/ROOT Thu Nov 03 21:09:37 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"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Demo_LIPIcs/ROOT Thu Nov 03 21:09:37 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"
--- a/src/Doc/ROOT Wed Nov 02 18:58:38 2022 +0100
+++ b/src/Doc/ROOT Thu Nov 03 21:09:37 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"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/ROOTS Thu Nov 03 21:09:37 2022 +0100
@@ -0,0 +1,3 @@
+Demo_Easychair
+Demo_FoilTeX
+Demo_LIPIcs
--- a/src/Pure/Isar/isar_cmd.ML Wed Nov 02 18:58:38 2022 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Thu Nov 03 21:09:37 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;
--- a/src/Pure/Isar/toplevel.ML Wed Nov 02 18:58:38 2022 +0100
+++ b/src/Pure/Isar/toplevel.ML Thu Nov 03 21:09:37 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
--- a/src/Pure/PIDE/command.ML Wed Nov 02 18:58:38 2022 +0100
+++ b/src/Pure/PIDE/command.ML Thu Nov 03 21:09:37 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);
--- a/src/Pure/PIDE/document.ML Wed Nov 02 18:58:38 2022 +0100
+++ b/src/Pure/PIDE/document.ML Thu Nov 03 21:09:37 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;
--- a/src/Pure/PIDE/query_operation.ML Wed Nov 02 18:58:38 2022 +0100
+++ b/src/Pure/PIDE/query_operation.ML Thu Nov 03 21:09:37 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;
--- a/src/Pure/PIDE/session.ML Wed Nov 02 18:58:38 2022 +0100
+++ b/src/Pure/PIDE/session.ML Thu Nov 03 21:09:37 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;
--- a/src/Pure/PIDE/session.scala Wed Nov 02 18:58:38 2022 +0100
+++ b/src/Pure/PIDE/session.scala Thu Nov 03 21:09:37 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] = {
--- a/src/Pure/Thy/document_output.ML Wed Nov 02 18:58:38 2022 +0100
+++ b/src/Pure/Thy/document_output.ML Thu Nov 03 21:09:37 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"
--- a/src/Pure/Thy/thy_info.ML Wed Nov 02 18:58:38 2022 +0100
+++ b/src/Pure/Thy/thy_info.ML Thu Nov 03 21:09:37 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;
--- a/src/Pure/Tools/print_operation.ML Wed Nov 02 18:58:38 2022 +0100
+++ b/src/Pure/Tools/print_operation.ML Thu Nov 03 21:09:37 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;
--- a/src/ZF/WF.thy Wed Nov 02 18:58:38 2022 +0100
+++ b/src/ZF/WF.thy Thu Nov 03 21:09:37 2022 +0100
@@ -361,12 +361,11 @@
wfrec[A](r,a,H) = H(a, \<lambda>x\<in>(r-``{a}) \<inter> 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\<open>Minimal-element characterization of well-foundedness\<close>
-lemma wf_eq_minimal:
- "wf(r) \<longleftrightarrow> (\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. \<langle>y,z\<rangle>:r \<longrightarrow> y\<notin>Q))"
-by (unfold wf_def, blast)
+lemma wf_eq_minimal: "wf(r) \<longleftrightarrow> (\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. \<langle>y,z\<rangle>:r \<longrightarrow> y\<notin>Q))"
+ unfolding wf_def by blast
end