src/Pure/Thy/thy_header.ML
changeset 58908 58bedbc18915
parent 58907 0ee3563803c9
child 58918 8d36bc5eaed3
equal deleted inserted replaced
58907:0ee3563803c9 58908:58bedbc18915
   129 
   129 
   130 
   130 
   131 (* read header *)
   131 (* read header *)
   132 
   132 
   133 val heading =
   133 val heading =
   134   (Parse.command_name headerN ||
   134   (Parse.command headerN ||
   135     Parse.command_name chapterN ||
   135     Parse.command chapterN ||
   136     Parse.command_name sectionN ||
   136     Parse.command sectionN ||
   137     Parse.command_name subsectionN ||
   137     Parse.command subsectionN ||
   138     Parse.command_name subsubsectionN) --
   138     Parse.command subsubsectionN) --
   139   Parse.tags -- Parse.!!! Parse.document_source;
   139   Parse.tags -- Parse.!!! Parse.document_source;
   140 
   140 
   141 val header =
   141 val header =
   142   (Scan.repeat heading -- Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
   142   (Scan.repeat heading -- Parse.command theoryN -- Parse.tags) |-- Parse.!!! args;
   143 
   143 
   144 fun token_source pos str =
   144 fun token_source pos str =
   145   str
   145   str
   146   |> Source.of_string_limited 8000
   146   |> Source.of_string_limited 8000
   147   |> Symbol.source
   147   |> Symbol.source