tuned;
authorwenzelm
Tue Aug 03 19:04:20 1999 +0200 (1999-08-03 ago)
changeset 71729ecd66cf546d
parent 7171 2a245a80a2c5
child 7173 bd1749e3a583
tuned;
added sect, subsect, subsubsect;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Aug 03 19:04:02 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Aug 03 19:04:20 1999 +0200
     1.3 @@ -39,12 +39,6 @@
     1.4  
     1.5  (** formal comments **)
     1.6  
     1.7 -val txtP = OuterSyntax.command "txt" "formal comment (proof)" K.prf_decl
     1.8 -  (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt)));
     1.9 -
    1.10 -val textP = OuterSyntax.command "text" "formal comment (theory)" K.thy_decl
    1.11 -  (P.comment >> (Toplevel.theory o IsarThy.add_text));
    1.12 -
    1.13  val titleP = OuterSyntax.command "title" "document title" K.thy_heading
    1.14    ((P.comment -- Scan.optional P.comment Comment.none -- Scan.optional P.comment Comment.none)
    1.15      >> (fn ((x, y), z) => Toplevel.theory (IsarThy.add_title x y z)));
    1.16 @@ -61,6 +55,22 @@
    1.17  val subsubsectionP = OuterSyntax.command "subsubsection" "subsubsection heading" K.thy_heading
    1.18    (P.comment >> (Toplevel.theory o IsarThy.add_subsubsection));
    1.19  
    1.20 +val textP = OuterSyntax.command "text" "formal comment (theory)" K.thy_decl
    1.21 +  (P.comment >> (Toplevel.theory o IsarThy.add_text));
    1.22 +
    1.23 +
    1.24 +val sectP = OuterSyntax.command "sect" "formal comment (proof)" K.prf_decl
    1.25 +  (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_sect)));
    1.26 +
    1.27 +val subsectP = OuterSyntax.command "subsect" "formal comment (proof)" K.prf_decl
    1.28 +  (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsect)));
    1.29 +
    1.30 +val subsubsectP = OuterSyntax.command "subsubsect" "formal comment (proof)" K.prf_decl
    1.31 +  (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsubsect)));
    1.32 +
    1.33 +val txtP = OuterSyntax.command "txt" "formal comment (proof)" K.prf_decl
    1.34 +  (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt)));
    1.35 +
    1.36  
    1.37  
    1.38  (** theory sections **)
    1.39 @@ -182,10 +192,6 @@
    1.40    OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
    1.41      (Scan.succeed (Toplevel.theory PureThy.local_path));
    1.42  
    1.43 -val pathP =
    1.44 -  OuterSyntax.command "path" "modify name-space entry path" K.thy_decl
    1.45 -    (P.xname >> (Toplevel.theory o Theory.add_path));
    1.46 -
    1.47  
    1.48  (* use ML text *)
    1.49  
    1.50 @@ -355,7 +361,7 @@
    1.51      (P.marg_comment >> IsarThy.default_proof);
    1.52  
    1.53  val skip_proofP =
    1.54 -  OuterSyntax.command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
    1.55 +  OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
    1.56      (P.marg_comment >> IsarThy.skip_proof);
    1.57  
    1.58  
    1.59 @@ -548,22 +554,24 @@
    1.60    outer_parse.ML, otherwise be prepared for unexpected errors*)
    1.61  
    1.62  val keywords =
    1.63 - ["!", "!!", "%", "(", ")", "*", "+", ",", "--", ":", "::", ";", "<",
    1.64 -  "<=", "=", "==", "=>", "?", "[", "]", "and", "as", "binder",
    1.65 + ["!", "!!", "%", "%%", "(", ")", "*", "+", ",", "--", ":", "::", ";",
    1.66 +  "<", "<=", "=", "==", "=>", "?", "[", "]", "and", "as", "binder",
    1.67    "concl", "files", "infixl", "infixr", "is", "output", "{", "|",
    1.68    "}"];
    1.69  
    1.70  val parsers = [
    1.71    (*theory structure*)
    1.72    theoryP, end_excursionP, kill_excursionP, contextP,
    1.73 +  (*formal comments*)
    1.74 +  titleP, chapterP, sectionP, subsectionP, subsubsectionP, textP,
    1.75 +  sectP, subsectP, subsubsectP, txtP,
    1.76    (*theory sections*)
    1.77 -  txtP, textP, titleP, chapterP, sectionP, subsectionP,
    1.78 -  subsubsectionP, classesP, classrelP, defaultsortP, typedeclP,
    1.79 -  typeabbrP, nontermP, aritiesP, constsP, syntaxP, translationsP,
    1.80 -  axiomsP, defsP, constdefsP, theoremsP, lemmasP, globalP, localP,
    1.81 -  pathP, useP, mlP, setupP, parse_ast_translationP,
    1.82 -  parse_translationP, print_translationP, typed_print_translationP,
    1.83 -  print_ast_translationP, token_translationP, oracleP,
    1.84 +  classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
    1.85 +  aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP,
    1.86 +  constdefsP, theoremsP, lemmasP, globalP, localP, useP, mlP, setupP,
    1.87 +  parse_ast_translationP, parse_translationP, print_translationP,
    1.88 +  typed_print_translationP, print_ast_translationP,
    1.89 +  token_translationP, oracleP,
    1.90    (*proof commands*)
    1.91    theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
    1.92    defP, fixP, letP, thenP, thenceP, fromP, withP, noteP, beginP, endP,
     2.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Aug 03 19:04:02 1999 +0200
     2.2 +++ b/src/Pure/Isar/isar_thy.ML	Tue Aug 03 19:04:20 1999 +0200
     2.3 @@ -7,13 +7,16 @@
     2.4  
     2.5  signature ISAR_THY =
     2.6  sig
     2.7 -  val add_txt: Comment.text -> ProofHistory.T -> ProofHistory.T
     2.8 -  val add_text: Comment.text -> theory -> theory
     2.9    val add_title: Comment.text -> Comment.text -> Comment.text -> theory -> theory
    2.10    val add_chapter: Comment.text -> theory -> theory
    2.11    val add_section: Comment.text -> theory -> theory
    2.12    val add_subsection: Comment.text -> theory -> theory
    2.13    val add_subsubsection: Comment.text -> theory -> theory
    2.14 +  val add_text: Comment.text -> theory -> theory
    2.15 +  val add_sect: Comment.text -> ProofHistory.T -> ProofHistory.T
    2.16 +  val add_subsect: Comment.text -> ProofHistory.T -> ProofHistory.T
    2.17 +  val add_subsubsect: Comment.text -> ProofHistory.T -> ProofHistory.T
    2.18 +  val add_txt: Comment.text -> ProofHistory.T -> ProofHistory.T
    2.19    val add_classes: (bclass * xclass list) list * Comment.text -> theory -> theory
    2.20    val add_classes_i: (bclass * class list) list * Comment.text  -> theory -> theory
    2.21    val add_classrel: (xclass * xclass) * Comment.text -> theory -> theory
    2.22 @@ -157,7 +160,6 @@
    2.23  
    2.24  (* formal comments *)
    2.25  
    2.26 -fun add_txt comment = ProofHistory.apply Proof.assert_forward;
    2.27  fun add_text comment thy = thy;
    2.28  fun add_title title author date thy = thy;
    2.29  val add_chapter = add_text;
    2.30 @@ -165,6 +167,11 @@
    2.31  val add_subsection = add_text;
    2.32  val add_subsubsection = add_text;
    2.33  
    2.34 +fun add_txt comment = ProofHistory.apply Proof.assert_forward;
    2.35 +val add_sect = add_text;
    2.36 +val add_subsect = add_text;
    2.37 +val add_subsubsect = add_text;
    2.38 +
    2.39  
    2.40  (* signature and syntax *)
    2.41