--- a/src/Pure/Isar/toplevel.ML Tue Jun 26 11:11:05 2018 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue Jun 26 14:01:46 2018 +0200
@@ -21,6 +21,7 @@
val theory_of: state -> theory
val proof_of: state -> Proof.state
val proof_position_of: state -> int
+ val is_end_theory: state -> bool
val end_theory: Position.T -> state -> theory
val presentation_context: state -> Proof.context
val presentation_state: Proof.context -> state
@@ -165,6 +166,9 @@
Proof (prf, _) => Proof_Node.position prf
| _ => ~1);
+fun is_end_theory (State (NONE, SOME (Theory (Context.Theory _, _)))) = true
+ | is_end_theory _ = false;
+
fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
| end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.here pos)
| end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.here pos);
--- a/src/Pure/Pure.thy Tue Jun 26 11:11:05 2018 +0200
+++ b/src/Pure/Pure.thy Tue Jun 26 14:01:46 2018 +0200
@@ -86,7 +86,7 @@
"prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
and "print_state" :: diag
and "welcome" :: diag
- and "end" :: thy_end % "theory"
+ and "end" :: thy_end
and "realizers" :: thy_decl
and "realizability" :: thy_decl
and "extract_type" "extract" :: thy_decl
--- a/src/Pure/Thy/thy_output.ML Tue Jun 26 11:11:05 2018 +0200
+++ b/src/Pure/Thy/thy_output.ML Tue Jun 26 14:01:46 2018 +0200
@@ -261,7 +261,7 @@
val active_tag' =
if is_some tag' then tag'
- else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE
+ else if cmd_name = "end" andalso Toplevel.is_end_theory state' then SOME "theory"
else
(case Keyword.command_tags keywords cmd_name @ document_tags of
default_tag :: _ => SOME default_tag