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