renamed verbatim/verb to text_raw/txt_raw;
authorwenzelm
Thu Oct 14 12:47:54 1999 +0200 (1999-10-14 ago)
changeset 78623e75fbd4a46b
parent 7861 8d5d3163fd81
child 7863 8b0aca9bdc26
renamed verbatim/verb to text_raw/txt_raw;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Oct 14 12:46:30 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Oct 14 12:47:54 1999 +0200
     1.3 @@ -58,8 +58,8 @@
     1.4  val textP = OuterSyntax.markup_command "text" "formal comment (theory)" K.thy_decl
     1.5    (P.comment >> (Toplevel.theory o IsarThy.add_text));
     1.6  
     1.7 -val verbatimP = OuterSyntax.verbatim_command "verbatim" "verbatim document preparation text"
     1.8 -  K.thy_decl (P.comment >> (Toplevel.theory o IsarThy.add_verbatim));
     1.9 +val text_rawP = OuterSyntax.verbatim_command "text_raw" "raw document preparation text"
    1.10 +  K.thy_decl (P.comment >> (Toplevel.theory o IsarThy.add_text_raw));
    1.11  
    1.12  
    1.13  val sectP = OuterSyntax.markup_command "sect" "formal comment (proof)" K.prf_decl
    1.14 @@ -74,8 +74,8 @@
    1.15  val txtP = OuterSyntax.markup_command "txt" "formal comment (proof)" K.prf_decl
    1.16    (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt)));
    1.17  
    1.18 -val verbP = OuterSyntax.verbatim_command "verb" "verbatim document preparation text (proof)"
    1.19 -  K.prf_decl (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_verb)));
    1.20 +val txt_rawP = OuterSyntax.verbatim_command "txt_raw" "raw document preparation text (proof)"
    1.21 +  K.prf_decl (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt_raw)));
    1.22  
    1.23  
    1.24  
    1.25 @@ -607,7 +607,7 @@
    1.26    theoryP, end_excursionP, kill_excursionP, contextP,
    1.27    (*markup commands*)
    1.28    headerP, chapterP, sectionP, subsectionP, subsubsectionP, textP,
    1.29 -  verbatimP, sectP, subsectP, subsubsectP, txtP, verbP,
    1.30 +  text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP,
    1.31    (*theory sections*)
    1.32    classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
    1.33    aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP,
     2.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Oct 14 12:46:30 1999 +0200
     2.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Oct 14 12:47:54 1999 +0200
     2.3 @@ -13,12 +13,12 @@
     2.4    val add_subsection: Comment.text -> theory -> theory
     2.5    val add_subsubsection: Comment.text -> theory -> theory
     2.6    val add_text: Comment.text -> theory -> theory
     2.7 -  val add_verbatim: Comment.text -> theory -> theory
     2.8 +  val add_text_raw: Comment.text -> theory -> theory
     2.9    val add_sect: Comment.text -> ProofHistory.T -> ProofHistory.T
    2.10    val add_subsect: Comment.text -> ProofHistory.T -> ProofHistory.T
    2.11    val add_subsubsect: Comment.text -> ProofHistory.T -> ProofHistory.T
    2.12    val add_txt: Comment.text -> ProofHistory.T -> ProofHistory.T
    2.13 -  val add_verb: Comment.text -> ProofHistory.T -> ProofHistory.T
    2.14 +  val add_txt_raw: Comment.text -> ProofHistory.T -> ProofHistory.T
    2.15    val add_classes: (bclass * xclass list) list * Comment.text -> theory -> theory
    2.16    val add_classes_i: (bclass * class list) list * Comment.text  -> theory -> theory
    2.17    val add_classrel: (xclass * xclass) * Comment.text -> theory -> theory
    2.18 @@ -172,7 +172,7 @@
    2.19    Toplevel.keep (fn state => if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF);
    2.20  
    2.21  fun add_text comment thy = thy:theory;
    2.22 -val add_verbatim = add_text;
    2.23 +val add_text_raw = add_text;
    2.24  val add_chapter = add_text;
    2.25  
    2.26  fun gen_add_section add present txt thy =
    2.27 @@ -183,7 +183,7 @@
    2.28  val add_subsubsection = gen_add_section add_text Present.subsubsection;
    2.29  
    2.30  fun add_txt comment = ProofHistory.apply Proof.assert_forward;
    2.31 -val add_verb = add_txt;
    2.32 +val add_txt_raw = add_txt;
    2.33  val add_sect = add_txt;
    2.34  val add_subsect = add_txt;
    2.35  val add_subsubsect = add_txt;