clarified default tag;
authorwenzelm
Tue Jun 26 14:01:46 2018 +0200 (13 months ago)
changeset 68505088780aa2b70
parent 68504 3524d60b8f15
child 68506 cef6c6b009fb
clarified default tag;
src/Pure/Isar/toplevel.ML
src/Pure/Pure.thy
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Jun 26 11:11:05 2018 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Jun 26 14:01:46 2018 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4    val theory_of: state -> theory
     1.5    val proof_of: state -> Proof.state
     1.6    val proof_position_of: state -> int
     1.7 +  val is_end_theory: state -> bool
     1.8    val end_theory: Position.T -> state -> theory
     1.9    val presentation_context: state -> Proof.context
    1.10    val presentation_state: Proof.context -> state
    1.11 @@ -165,6 +166,9 @@
    1.12      Proof (prf, _) => Proof_Node.position prf
    1.13    | _ => ~1);
    1.14  
    1.15 +fun is_end_theory (State (NONE, SOME (Theory (Context.Theory _, _)))) = true
    1.16 +  | is_end_theory _ = false;
    1.17 +
    1.18  fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
    1.19    | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.here pos)
    1.20    | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.here pos);
     2.1 --- a/src/Pure/Pure.thy	Tue Jun 26 11:11:05 2018 +0200
     2.2 +++ b/src/Pure/Pure.thy	Tue Jun 26 14:01:46 2018 +0200
     2.3 @@ -86,7 +86,7 @@
     2.4      "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
     2.5    and "print_state" :: diag
     2.6    and "welcome" :: diag
     2.7 -  and "end" :: thy_end % "theory"
     2.8 +  and "end" :: thy_end
     2.9    and "realizers" :: thy_decl
    2.10    and "realizability" :: thy_decl
    2.11    and "extract_type" "extract" :: thy_decl
     3.1 --- a/src/Pure/Thy/thy_output.ML	Tue Jun 26 11:11:05 2018 +0200
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Jun 26 14:01:46 2018 +0200
     3.3 @@ -261,7 +261,7 @@
     3.4  
     3.5      val active_tag' =
     3.6        if is_some tag' then tag'
     3.7 -      else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE
     3.8 +      else if cmd_name = "end" andalso Toplevel.is_end_theory state' then SOME "theory"
     3.9        else
    3.10          (case Keyword.command_tags keywords cmd_name @ document_tags of
    3.11            default_tag :: _ => SOME default_tag