tuned signature;
authorwenzelm
Tue Dec 05 14:03:10 2017 +0100 (4 months ago)
changeset 671361368cfa92b7a
parent 67134 66ce07e8dbf2
child 67137 f2384ad1dff4
tuned signature;
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/parse.ML
src/Pure/Thy/thy_header.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Dec 04 23:10:52 2017 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Dec 05 14:03:10 2017 +0100
     1.3 @@ -183,10 +183,10 @@
     1.4    Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false));
     1.5  
     1.6  fun parse_command thy =
     1.7 -  Scan.ahead (before_command |-- Parse.position Parse.command_) :|-- (fn (name, pos) =>
     1.8 +  Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) =>
     1.9      let
    1.10        val keywords = Thy_Header.get_keywords thy;
    1.11 -      val command_tags = Parse.command_ -- Parse.tags;
    1.12 +      val command_tags = Parse.command -- Parse.tags;
    1.13        val tr0 =
    1.14          Toplevel.empty
    1.15          |> Toplevel.name name
     2.1 --- a/src/Pure/Isar/parse.ML	Mon Dec 04 23:10:52 2017 +0100
     2.2 +++ b/src/Pure/Isar/parse.ML	Tue Dec 05 14:03:10 2017 +0100
     2.3 @@ -15,7 +15,7 @@
     2.4    val position: 'a parser -> ('a * Position.T) parser
     2.5    val input: 'a parser -> Input.source parser
     2.6    val inner_syntax: 'a parser -> string parser
     2.7 -  val command_: string parser
     2.8 +  val command: string parser
     2.9    val keyword: string parser
    2.10    val short_ident: string parser
    2.11    val long_ident: string parser
    2.12 @@ -32,7 +32,7 @@
    2.13    val verbatim: string parser
    2.14    val cartouche: string parser
    2.15    val eof: string parser
    2.16 -  val command: string -> string parser
    2.17 +  val command_name: string -> string parser
    2.18    val keyword_with: (string -> bool) -> string parser
    2.19    val keyword_markup: bool * Markup.T -> string -> string parser
    2.20    val keyword_improper: string -> string parser
    2.21 @@ -173,7 +173,7 @@
    2.22    group (fn () => Token.str_of_kind k)
    2.23      (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
    2.24  
    2.25 -val command_ = kind Token.Command;
    2.26 +val command = kind Token.Command;
    2.27  val keyword = kind Token.Keyword;
    2.28  val short_ident = kind Token.Ident;
    2.29  val long_ident = kind Token.Long_Ident;
    2.30 @@ -189,7 +189,7 @@
    2.31  val cartouche = kind Token.Cartouche;
    2.32  val eof = kind Token.EOF;
    2.33  
    2.34 -fun command x =
    2.35 +fun command_name x =
    2.36    group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x)
    2.37      (RESET_VALUE (Scan.one (fn tok => Token.is_command tok andalso Token.content_of tok = x)))
    2.38    >> Token.content_of;
     3.1 --- a/src/Pure/Thy/thy_header.ML	Mon Dec 04 23:10:52 2017 +0100
     3.2 +++ b/src/Pure/Thy/thy_header.ML	Tue Dec 05 14:03:10 2017 +0100
     3.3 @@ -160,19 +160,19 @@
     3.4  (* read header *)
     3.5  
     3.6  val heading =
     3.7 -  (Parse.command chapterN ||
     3.8 -    Parse.command sectionN ||
     3.9 -    Parse.command subsectionN ||
    3.10 -    Parse.command subsubsectionN ||
    3.11 -    Parse.command paragraphN ||
    3.12 -    Parse.command subparagraphN ||
    3.13 -    Parse.command textN ||
    3.14 -    Parse.command txtN ||
    3.15 -    Parse.command text_rawN) --
    3.16 +  (Parse.command_name chapterN ||
    3.17 +    Parse.command_name sectionN ||
    3.18 +    Parse.command_name subsectionN ||
    3.19 +    Parse.command_name subsubsectionN ||
    3.20 +    Parse.command_name paragraphN ||
    3.21 +    Parse.command_name subparagraphN ||
    3.22 +    Parse.command_name textN ||
    3.23 +    Parse.command_name txtN ||
    3.24 +    Parse.command_name text_rawN) --
    3.25    Parse.tags -- Parse.!!! Parse.document_source;
    3.26  
    3.27  val header =
    3.28 -  (Scan.repeat heading -- Parse.command theoryN -- Parse.tags) |-- Parse.!!! args;
    3.29 +  (Scan.repeat heading -- Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
    3.30  
    3.31  fun token_source pos =
    3.32    Symbol.explode