clarified modules;
authorwenzelm
Fri Mar 08 17:05:23 2019 +0100 (6 weeks ago ago)
changeset 70057b49bd228ac8a
parent 70056 03bc14eab432
child 70058 45b2e784350a
clarified modules;
uniform "tag" parser;
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/parse.ML
src/Pure/ROOT.ML
src/Pure/Thy/document_source.ML
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Mar 07 16:59:12 2019 +0000
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Mar 08 17:05:23 2019 +0100
     1.3 @@ -185,7 +185,7 @@
     1.4    Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) =>
     1.5      let
     1.6        val keywords = Thy_Header.get_keywords thy;
     1.7 -      val command_tags = Parse.command -- Parse.tags;
     1.8 +      val command_tags = Parse.command -- Document_Source.tags;
     1.9        val tr0 =
    1.10          Toplevel.empty
    1.11          |> Toplevel.name name
     2.1 --- a/src/Pure/Isar/parse.ML	Thu Mar 07 16:59:12 2019 +0000
     2.2 +++ b/src/Pure/Isar/parse.ML	Fri Mar 08 17:05:23 2019 +0100
     2.3 @@ -42,8 +42,6 @@
     2.4    val underscore: string parser
     2.5    val maybe: 'a parser -> 'a option parser
     2.6    val maybe_position: ('a * Position.T) parser -> ('a option * Position.T) parser
     2.7 -  val tag_name: string parser
     2.8 -  val tags: string list parser
     2.9    val opt_keyword: string -> bool parser
    2.10    val opt_bang: bool parser
    2.11    val begin: string parser
    2.12 @@ -227,9 +225,6 @@
    2.13  val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
    2.14  val real = float_number >> Value.parse_real || int >> Real.fromInt;
    2.15  
    2.16 -val tag_name = group (fn () => "tag name") (short_ident || string);
    2.17 -val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
    2.18 -
    2.19  fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
    2.20  val opt_bang = Scan.optional ($$$ "!" >> K true) false;
    2.21  
     3.1 --- a/src/Pure/ROOT.ML	Thu Mar 07 16:59:12 2019 +0000
     3.2 +++ b/src/Pure/ROOT.ML	Fri Mar 08 17:05:23 2019 +0100
     3.3 @@ -206,6 +206,7 @@
     3.4  ML_file "Isar/keyword.ML";
     3.5  ML_file "Isar/token.ML";
     3.6  ML_file "Isar/parse.ML";
     3.7 +ML_file "Thy/document_source.ML";
     3.8  ML_file "Thy/thy_header.ML";
     3.9  
    3.10  (*proof context*)
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/Thy/document_source.ML	Fri Mar 08 17:05:23 2019 +0100
     4.3 @@ -0,0 +1,51 @@
     4.4 +(*  Title:      Pure/Thy/document_source.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Document source for presentation.
     4.8 +*)
     4.9 +
    4.10 +signature DOCUMENT_SOURCE =
    4.11 +sig
    4.12 +  val is_white: Token.T -> bool
    4.13 +  val is_black: Token.T -> bool
    4.14 +  val is_white_comment: Token.T -> bool
    4.15 +  val is_black_comment: Token.T -> bool
    4.16 +  val is_improper: Token.T -> bool
    4.17 +  val improper: Token.T list parser
    4.18 +  val improper_end: Token.T list parser
    4.19 +  val blank_end: Token.T list parser
    4.20 +  val tag: string parser
    4.21 +  val tags: string list parser
    4.22 +end;
    4.23 +
    4.24 +structure Document_Source: DOCUMENT_SOURCE =
    4.25 +struct
    4.26 +
    4.27 +(* white space and comments *)
    4.28 +
    4.29 +(*NB: arranging white space around command spans is a black art*)
    4.30 +
    4.31 +val is_white = Token.is_space orf Token.is_informal_comment;
    4.32 +val is_black = not o is_white;
    4.33 +
    4.34 +val is_white_comment = Token.is_informal_comment;
    4.35 +val is_black_comment = Token.is_formal_comment;
    4.36 +
    4.37 +
    4.38 +val space_proper =
    4.39 +  Scan.one Token.is_blank -- Scan.many is_white_comment -- Scan.one is_black;
    4.40 +
    4.41 +val is_improper = not o (is_black orf Token.is_begin_ignore orf Token.is_end_ignore);
    4.42 +val improper = Scan.many is_improper;
    4.43 +val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
    4.44 +val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank));
    4.45 +
    4.46 +
    4.47 +(* tags *)
    4.48 +
    4.49 +val tag_name = Parse.group (fn () => "document tag name") (Parse.short_ident || Parse.string);
    4.50 +
    4.51 +val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (tag_name --| blank_end);
    4.52 +val tags = Scan.repeat tag;
    4.53 +
    4.54 +end;
     5.1 --- a/src/Pure/Thy/thy_header.ML	Thu Mar 07 16:59:12 2019 +0000
     5.2 +++ b/src/Pure/Thy/thy_header.ML	Fri Mar 08 17:05:23 2019 +0100
     5.3 @@ -137,7 +137,7 @@
     5.4  
     5.5  val keyword_spec =
     5.6    Parse.group (fn () => "outer syntax keyword specification")
     5.7 -    (Parse.name -- opt_files -- Parse.tags);
     5.8 +    (Parse.name -- opt_files -- Document_Source.tags);
     5.9  
    5.10  val keyword_decl =
    5.11    Scan.repeat1 Parse.string_position --
    5.12 @@ -175,10 +175,10 @@
    5.13      Parse.command_name textN ||
    5.14      Parse.command_name txtN ||
    5.15      Parse.command_name text_rawN) --
    5.16 -  Parse.tags -- Parse.!!! Parse.document_source;
    5.17 +  Document_Source.tags -- Parse.!!! Parse.document_source;
    5.18  
    5.19  val parse_header =
    5.20 -  (Scan.repeat heading -- Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
    5.21 +  (Scan.repeat heading -- Parse.command_name theoryN -- Document_Source.tags) |-- Parse.!!! args;
    5.22  
    5.23  fun read_tokens pos toks =
    5.24    filter Token.is_proper toks
     6.1 --- a/src/Pure/Thy/thy_output.ML	Thu Mar 07 16:59:12 2019 +0000
     6.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Mar 08 17:05:23 2019 +0100
     6.3 @@ -170,15 +170,6 @@
     6.4  
     6.5  (** present theory source **)
     6.6  
     6.7 -(*NB: arranging white space around command spans is a black art*)
     6.8 -
     6.9 -val is_white = Token.is_space orf Token.is_informal_comment;
    6.10 -val is_black = not o is_white;
    6.11 -
    6.12 -val is_white_comment = Token.is_informal_comment;
    6.13 -val is_black_comment = Token.is_formal_comment;
    6.14 -
    6.15 -
    6.16  (* presentation tokens *)
    6.17  
    6.18  datatype token =
    6.19 @@ -191,8 +182,8 @@
    6.20  fun basic_token pred (Basic_Token tok) = pred tok
    6.21    | basic_token _ _ = false;
    6.22  
    6.23 -val white_token = basic_token is_white;
    6.24 -val white_comment_token = basic_token is_white_comment;
    6.25 +val white_token = basic_token Document_Source.is_white;
    6.26 +val white_comment_token = basic_token Document_Source.is_white_comment;
    6.27  val blank_token = basic_token Token.is_blank;
    6.28  val newline_token = basic_token Token.is_newline;
    6.29  
    6.30 @@ -348,14 +339,6 @@
    6.31  val markup_true = "\\isamarkuptrue%\n";
    6.32  val markup_false = "\\isamarkupfalse%\n";
    6.33  
    6.34 -val space_proper =
    6.35 -  Scan.one Token.is_blank -- Scan.many is_white_comment -- Scan.one is_black;
    6.36 -
    6.37 -val is_improper = not o (is_black orf Token.is_begin_ignore orf Token.is_end_ignore);
    6.38 -val improper = Scan.many is_improper;
    6.39 -val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
    6.40 -val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank));
    6.41 -
    6.42  val opt_newline = Scan.option (Scan.one Token.is_newline);
    6.43  
    6.44  val ignore =
    6.45 @@ -365,11 +348,10 @@
    6.46      (if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline)
    6.47      >> pair (d - 1));
    6.48  
    6.49 -val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end);
    6.50 -
    6.51  val locale =
    6.52 -  Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
    6.53 -    Parse.!!! (improper |-- Parse.name --| (improper -- Parse.$$$ ")")));
    6.54 +  Scan.option ((Parse.$$$ "(" -- Document_Source.improper -- Parse.$$$ "in") |--
    6.55 +    Parse.!!!
    6.56 +      (Document_Source.improper |-- Parse.name --| (Document_Source.improper -- Parse.$$$ ")")));
    6.57  
    6.58  in
    6.59  
    6.60 @@ -386,25 +368,26 @@
    6.61        >> (fn d => (NONE, (Ignore_Token, ("", d))));
    6.62  
    6.63      fun markup pred mk flag = Scan.peek (fn d =>
    6.64 -      improper |--
    6.65 +      Document_Source.improper |--
    6.66          Parse.position (Scan.one (fn tok =>
    6.67            Token.is_command tok andalso pred keywords (Token.content_of tok))) --
    6.68 -      Scan.repeat tag --
    6.69 -      Parse.!!!! ((improper -- locale -- improper) |-- Parse.document_source --| improper_end)
    6.70 -      >> (fn (((tok, pos'), tags), source) =>
    6.71 -        let val name = Token.content_of tok
    6.72 -        in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end));
    6.73 +      Scan.repeat Document_Source.tag --
    6.74 +      Parse.!!!! ((Document_Source.improper -- locale -- Document_Source.improper) |--
    6.75 +        Parse.document_source --| Document_Source.improper_end)
    6.76 +          >> (fn (((tok, pos'), tags), source) =>
    6.77 +            let val name = Token.content_of tok
    6.78 +            in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end));
    6.79  
    6.80      val command = Scan.peek (fn d =>
    6.81 -      Scan.optional (Scan.one Token.is_command_modifier ::: improper) [] --
    6.82 -      Scan.one Token.is_command -- Scan.repeat tag
    6.83 +      Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] --
    6.84 +      Scan.one Token.is_command -- Document_Source.tags
    6.85        >> (fn ((cmd_mod, cmd), tags) =>
    6.86          map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
    6.87            [(SOME (Token.content_of cmd, Token.pos_of cmd, tags),
    6.88              (Basic_Token cmd, (markup_false, d)))]));
    6.89  
    6.90      val cmt = Scan.peek (fn d =>
    6.91 -      Scan.one is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
    6.92 +      Scan.one Document_Source.is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
    6.93  
    6.94      val other = Scan.peek (fn d =>
    6.95         Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));