src/Pure/Isar/isar_thy.ML
changeset 7734 9c098c777926
parent 7678 027b6ec2f084
child 7775 26898fbd19ca
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Oct 05 15:36:28 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Tue Oct 05 15:36:56 1999 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature ISAR_THY =
     1.6  sig
     1.7 -  val add_title: Comment.text -> Comment.text -> Comment.text -> theory -> theory
     1.8 +  val add_header: Comment.text -> Toplevel.transition -> Toplevel.transition
     1.9    val add_chapter: Comment.text -> theory -> theory
    1.10    val add_section: Comment.text -> theory -> theory
    1.11    val add_subsection: Comment.text -> theory -> theory
    1.12 @@ -166,8 +166,10 @@
    1.13  
    1.14  (* formal comments *)
    1.15  
    1.16 +fun add_header comment =
    1.17 +  Toplevel.keep (fn state => if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF);
    1.18 +
    1.19  fun add_text comment thy = thy:theory;
    1.20 -fun add_title title author date thy = thy;
    1.21  val add_chapter = add_text;
    1.22  
    1.23  fun gen_add_section add present txt thy =
    1.24 @@ -512,10 +514,7 @@
    1.25  
    1.26  val begin_theory = gen_begin_theory ThyInfo.begin_theory;
    1.27  val begin_update_theory = gen_begin_theory ThyInfo.begin_update_theory;
    1.28 -
    1.29 -fun end_theory thy =
    1.30 -  (Present.end_theory (PureThy.get_name thy); ThyInfo.end_theory thy);
    1.31 -
    1.32 +val end_theory = ThyInfo.end_theory;
    1.33  fun kill_theory thy = ThyInfo.remove_thy (PureThy.get_name thy);
    1.34  
    1.35