present chapter;
authorwenzelm
Wed Jan 05 11:41:38 2000 +0100 (2000-01-05 ago)
changeset 80905a241706d9b3
parent 8089 8efec140c5e4
child 8091 226dcdc3c5f3
present chapter;
tuned proof markup commands;
moved obtain to obtain.ML;
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Wed Jan 05 11:40:13 2000 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed Jan 05 11:41:38 2000 +0100
     1.3 @@ -137,12 +137,6 @@
     1.4      -> Toplevel.transition -> Toplevel.transition
     1.5    val finally_i: (thm list * Comment.interest) option * Comment.text
     1.6      -> Toplevel.transition -> Toplevel.transition
     1.7 -  val obtain: ((string list * string option) * Comment.text) list
     1.8 -    * ((string * Args.src list * (string * (string list * string list)) list)
     1.9 -      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.10 -  val obtain_i: ((string list * typ option) * Comment.text) list
    1.11 -    * ((string * Proof.context attribute list * (term * (term list * term list)) list)
    1.12 -      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.13    val use_mltext: string -> bool -> theory option -> unit
    1.14    val use_mltext_theory: string -> bool -> theory -> theory
    1.15    val use_setup: string -> theory -> theory
    1.16 @@ -168,24 +162,24 @@
    1.17  
    1.18  (** derived theory and proof operations **)
    1.19  
    1.20 -(* formal comments *)
    1.21 +(* markup commands *)
    1.22  
    1.23  fun add_header comment =
    1.24    Toplevel.keep (fn state => if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF);
    1.25  
    1.26 -fun add_text comment thy = thy:theory;
    1.27 +fun add_text _ x = x;
    1.28  fun add_text_raw _ x = x;
    1.29 -val add_chapter = add_text;
    1.30  
    1.31 -fun gen_add_section add present txt thy =
    1.32 +fun add_heading add present txt thy =
    1.33    (Context.setmp (Some thy) present (Comment.string_of txt); add txt thy);
    1.34  
    1.35 -val add_section = gen_add_section add_text Present.section;
    1.36 -val add_subsection = gen_add_section add_text Present.subsection;
    1.37 -val add_subsubsection = gen_add_section add_text Present.subsubsection;
    1.38 +val add_chapter = add_heading add_text Present.section;
    1.39 +val add_section = add_heading add_text Present.section;
    1.40 +val add_subsection = add_heading add_text Present.subsection;
    1.41 +val add_subsubsection = add_heading add_text Present.subsubsection;
    1.42  
    1.43 -fun add_txt comment = ProofHistory.apply Proof.assert_forward;
    1.44 -val add_txt_raw = add_text_raw;
    1.45 +fun add_txt (_: Comment.text) = ProofHistory.apply I;
    1.46 +val add_txt_raw = add_txt;
    1.47  val add_sect = add_txt;
    1.48  val add_subsect = add_txt;
    1.49  val add_subsubsect = add_txt;
    1.50 @@ -295,9 +289,6 @@
    1.51  
    1.52  (* statements *)
    1.53  
    1.54 -fun multi_local_attribute state (name, src, s) =
    1.55 -  (name, map (Attrib.local_attribute (Proof.theory_of state)) src, s);
    1.56 -
    1.57  local
    1.58  
    1.59  fun global_statement f (name, src, s) int thy =
    1.60 @@ -312,6 +303,9 @@
    1.61  
    1.62  fun local_statement_i f g (name, atts, t) = ProofHistory.apply (f name atts t o g);
    1.63  
    1.64 +fun multi_local_attribute state (name, src, s) =
    1.65 +  (name, map (Attrib.local_attribute (Proof.theory_of state)) src, s);
    1.66 +
    1.67  fun multi_statement f args = ProofHistory.apply (fn state =>
    1.68    f (map (multi_local_attribute state) args) state);
    1.69  
    1.70 @@ -449,16 +443,6 @@
    1.71  end;
    1.72  
    1.73  
    1.74 -(* obtain *)
    1.75 -
    1.76 -fun obtain (xs, asms) = ProofHistory.applys (fn state =>
    1.77 -  Obtain.obtain (map Comment.ignore xs)
    1.78 -    (map (multi_local_attribute state o Comment.ignore) asms) state);
    1.79 -
    1.80 -fun obtain_i (xs, asms) = ProofHistory.applys
    1.81 -  (Obtain.obtain_i (map Comment.ignore xs) (map Comment.ignore asms));
    1.82 -
    1.83 -
    1.84  (* use ML text *)
    1.85  
    1.86  fun use_mltext txt verb opt_thy = Context.setmp opt_thy (use_text writeln verb) txt;