src/Pure/Thy/thy_header.ML
changeset 63429 baedd4724f08
parent 63022 785a59235a15
child 63448 998acd66fbd7
     1.1 --- a/src/Pure/Thy/thy_header.ML	Fri Jul 08 22:22:51 2016 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.ML	Sun Jul 10 11:18:35 2016 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature THY_HEADER =
     1.6  sig
     1.7 -  type keywords = ((string * Position.T) * Keyword.spec option) list
     1.8 +  type keywords = ((string * Position.T) * Keyword.spec) list
     1.9    type header =
    1.10     {name: string * Position.T,
    1.11      imports: (string * Position.T) list,
    1.12 @@ -32,7 +32,7 @@
    1.13  
    1.14  (* header *)
    1.15  
    1.16 -type keywords = ((string * Position.T) * Keyword.spec option) list;
    1.17 +type keywords = ((string * Position.T) * Keyword.spec) list;
    1.18  
    1.19  type header =
    1.20   {name: string * Position.T,
    1.21 @@ -63,27 +63,27 @@
    1.22  val bootstrap_keywords =
    1.23    Keyword.empty_keywords
    1.24    |> Keyword.add_keywords
    1.25 -    [(("%", @{here}), NONE),
    1.26 -     (("(", @{here}), NONE),
    1.27 -     ((")", @{here}), NONE),
    1.28 -     ((",", @{here}), NONE),
    1.29 -     (("::", @{here}), NONE),
    1.30 -     (("==", @{here}), NONE),
    1.31 -     (("and", @{here}), NONE),
    1.32 -     ((beginN, @{here}), NONE),
    1.33 -     ((importsN, @{here}), NONE),
    1.34 -     ((keywordsN, @{here}), NONE),
    1.35 -     ((chapterN, @{here}), SOME ((Keyword.document_heading, []), [])),
    1.36 -     ((sectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
    1.37 -     ((subsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
    1.38 -     ((subsubsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
    1.39 -     ((paragraphN, @{here}), SOME ((Keyword.document_heading, []), [])),
    1.40 -     ((subparagraphN, @{here}), SOME ((Keyword.document_heading, []), [])),
    1.41 -     ((textN, @{here}), SOME ((Keyword.document_body, []), [])),
    1.42 -     ((txtN, @{here}), SOME ((Keyword.document_body, []), [])),
    1.43 -     ((text_rawN, @{here}), SOME ((Keyword.document_raw, []), [])),
    1.44 -     ((theoryN, @{here}), SOME ((Keyword.thy_begin, []), ["theory"])),
    1.45 -     (("ML", @{here}), SOME ((Keyword.thy_decl, []), ["ML"]))];
    1.46 +    [(("%", @{here}), Keyword.no_spec),
    1.47 +     (("(", @{here}), Keyword.no_spec),
    1.48 +     ((")", @{here}), Keyword.no_spec),
    1.49 +     ((",", @{here}), Keyword.no_spec),
    1.50 +     (("::", @{here}), Keyword.no_spec),
    1.51 +     (("==", @{here}), Keyword.no_spec),
    1.52 +     (("and", @{here}), Keyword.no_spec),
    1.53 +     ((beginN, @{here}), Keyword.no_spec),
    1.54 +     ((importsN, @{here}), Keyword.no_spec),
    1.55 +     ((keywordsN, @{here}), Keyword.no_spec),
    1.56 +     ((chapterN, @{here}), ((Keyword.document_heading, []), [])),
    1.57 +     ((sectionN, @{here}), ((Keyword.document_heading, []), [])),
    1.58 +     ((subsectionN, @{here}), ((Keyword.document_heading, []), [])),
    1.59 +     ((subsubsectionN, @{here}), ((Keyword.document_heading, []), [])),
    1.60 +     ((paragraphN, @{here}), ((Keyword.document_heading, []), [])),
    1.61 +     ((subparagraphN, @{here}), ((Keyword.document_heading, []), [])),
    1.62 +     ((textN, @{here}), ((Keyword.document_body, []), [])),
    1.63 +     ((txtN, @{here}), ((Keyword.document_body, []), [])),
    1.64 +     ((text_rawN, @{here}), ((Keyword.document_raw, []), [])),
    1.65 +     ((theoryN, @{here}), ((Keyword.thy_begin, []), ["theory"])),
    1.66 +     (("ML", @{here}), ((Keyword.thy_decl, []), ["ML"]))];
    1.67  
    1.68  
    1.69  (* theory data *)
    1.70 @@ -133,7 +133,7 @@
    1.71  
    1.72  val keyword_decl =
    1.73    Scan.repeat1 (Parse.position Parse.string) --
    1.74 -  Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) --
    1.75 +  Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec --
    1.76    Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl)
    1.77    >> (fn ((names, spec), _) => map (rpair spec) names);
    1.78