chapter etc. headings;
authorwenzelm
Wed Nov 25 14:00:12 1998 +0100 (1998-11-25 ago)
changeset 5958c48efb523a4d
parent 5957 9c0c69ab7d02
child 5959 7af99477751b
chapter etc. headings;
use, use_thy, cd: name;
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Nov 25 13:59:06 1998 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Nov 25 14:00:12 1998 +0100
     1.3 @@ -12,8 +12,7 @@
     1.4    - result (interactive): print current result (?);
     1.5    - check evaluation of transformers (exns!);
     1.6    - 'result' command;
     1.7 -  - '--' (comment) option everywhere;
     1.8 -  - 'chapter', 'section' etc.;
     1.9 +  - '--' (comment) option almost everywhere:
    1.10    - 'thm': xthms1;
    1.11  *)
    1.12  
    1.13 @@ -53,7 +52,19 @@
    1.14  (* formal comments *)
    1.15  
    1.16  val textP = OuterSyntax.parser false "text" "formal comments"
    1.17 -  (text >> K (Toplevel.keep (K ())));
    1.18 +  (text >> (Toplevel.theory o IsarThy.add_text));
    1.19 +
    1.20 +val chapterP = OuterSyntax.parser false "chapter" "chapter heading"
    1.21 +  (text >> (Toplevel.theory o IsarThy.add_chapter));
    1.22 +
    1.23 +val sectionP = OuterSyntax.parser false "section" "section heading"
    1.24 +  (text >> (Toplevel.theory o IsarThy.add_section));
    1.25 +
    1.26 +val subsectionP = OuterSyntax.parser false "subsection" "subsection heading"
    1.27 +  (text >> (Toplevel.theory o IsarThy.add_subsection));
    1.28 +
    1.29 +val subsubsectionP = OuterSyntax.parser false "subsubsection" "subsubsection heading"
    1.30 +  (text >> (Toplevel.theory o IsarThy.add_subsubsection));
    1.31  
    1.32  
    1.33  (* classes and sorts *)
    1.34 @@ -196,7 +207,7 @@
    1.35  
    1.36  val useP =
    1.37    OuterSyntax.parser true "use" "eval ML text from file"
    1.38 -    (string >> IsarCmd.use);
    1.39 +    (name >> IsarCmd.use);
    1.40  
    1.41  val mlP =
    1.42    OuterSyntax.parser false "ML" "eval ML text"
    1.43 @@ -446,7 +457,7 @@
    1.44  
    1.45  val cdP =
    1.46    OuterSyntax.parser true "cd" "change current working directory"
    1.47 -    (string >> IsarCmd.cd);
    1.48 +    (name >> IsarCmd.cd);
    1.49  
    1.50  val pwdP =
    1.51    OuterSyntax.parser true "pwd" "print current working directory"
    1.52 @@ -454,7 +465,7 @@
    1.53  
    1.54  val use_thyP =
    1.55    OuterSyntax.parser true "use_thy" "use_thy theory file"
    1.56 -    (string >> IsarCmd.use_thy);
    1.57 +    (name >> IsarCmd.use_thy);
    1.58  
    1.59  val loadP =
    1.60    OuterSyntax.parser true "load" "load theory file"
    1.61 @@ -491,7 +502,7 @@
    1.62    outer_parse.ML, otherwise be prepared for unexpected errors*)
    1.63  
    1.64  val keywords =
    1.65 - ["(", ")", "*", "+", ",", ":", "::", ";", "<", "<=", "=", "==", "=>",
    1.66 + ["(", ")", "*", "+", "--", ",", ":", "::", ";", "<", "<=", "=", "==", "=>",
    1.67    "?", "[", "]", "and", "as", "binder", "infixl", "infixr", "is",
    1.68    "mixfix", "output", "{", "|", "}"];
    1.69  
    1.70 @@ -499,12 +510,13 @@
    1.71    (*theory structure*)
    1.72    contextP, theoryP, endP,
    1.73    (*theory sections*)
    1.74 -  textP, classesP, classrelP, defaultsortP, typedeclP, typeabbrP,
    1.75 -  nontermP, aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP,
    1.76 -  theoremsP, lemmasP, axclassP, instanceP, globalP, localP, pathP,
    1.77 -  useP, mlP, setupP, parse_ast_translationP, parse_translationP,
    1.78 -  print_translationP, typed_print_translationP,
    1.79 -  print_ast_translationP, token_translationP, oracleP,
    1.80 +  textP, chapterP, sectionP, subsectionP, subsubsectionP, classesP,
    1.81 +  classrelP, defaultsortP, typedeclP, typeabbrP, nontermP, aritiesP,
    1.82 +  constsP, syntaxP, translationsP, axiomsP, defsP, theoremsP, lemmasP,
    1.83 +  axclassP, instanceP, globalP, localP, pathP, useP, mlP, setupP,
    1.84 +  parse_ast_translationP, parse_translationP, print_translationP,
    1.85 +  typed_print_translationP, print_ast_translationP,
    1.86 +  token_translationP, oracleP,
    1.87    (*proof commands*)
    1.88    theoremP, lemmaP, showP, haveP, assumeP, fixP, letP, thenP, fromP,
    1.89    factsP, beginP, nextP, qedP, qed_withP, kill_proofP, refineP,