# HG changeset patch
# User wenzelm
# Date 1530014506 -7200
# Node ID 088780aa2b70426c989709c9193292920acfdb43
# Parent  3524d60b8f158072d561a0b32f9b5a80cb6a28c1
clarified default tag;

diff -r 3524d60b8f15 -r 088780aa2b70 src/Pure/Isar/toplevel.ML
--- 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);
diff -r 3524d60b8f15 -r 088780aa2b70 src/Pure/Pure.thy
--- 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
diff -r 3524d60b8f15 -r 088780aa2b70 src/Pure/Thy/thy_output.ML
--- 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