--- a/src/Pure/Isar/outer_syntax.ML Thu Mar 07 16:59:12 2019 +0000
+++ b/src/Pure/Isar/outer_syntax.ML Fri Mar 08 17:05:23 2019 +0100
@@ -185,7 +185,7 @@
Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) =>
let
val keywords = Thy_Header.get_keywords thy;
- val command_tags = Parse.command -- Parse.tags;
+ val command_tags = Parse.command -- Document_Source.tags;
val tr0 =
Toplevel.empty
|> Toplevel.name name
--- a/src/Pure/Isar/parse.ML Thu Mar 07 16:59:12 2019 +0000
+++ b/src/Pure/Isar/parse.ML Fri Mar 08 17:05:23 2019 +0100
@@ -42,8 +42,6 @@
val underscore: string parser
val maybe: 'a parser -> 'a option parser
val maybe_position: ('a * Position.T) parser -> ('a option * Position.T) parser
- val tag_name: string parser
- val tags: string list parser
val opt_keyword: string -> bool parser
val opt_bang: bool parser
val begin: string parser
@@ -227,9 +225,6 @@
val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
val real = float_number >> Value.parse_real || int >> Real.fromInt;
-val tag_name = group (fn () => "tag name") (short_ident || string);
-val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
-
fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
val opt_bang = Scan.optional ($$$ "!" >> K true) false;
--- a/src/Pure/ROOT.ML Thu Mar 07 16:59:12 2019 +0000
+++ b/src/Pure/ROOT.ML Fri Mar 08 17:05:23 2019 +0100
@@ -206,6 +206,7 @@
ML_file "Isar/keyword.ML";
ML_file "Isar/token.ML";
ML_file "Isar/parse.ML";
+ML_file "Thy/document_source.ML";
ML_file "Thy/thy_header.ML";
(*proof context*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/document_source.ML Fri Mar 08 17:05:23 2019 +0100
@@ -0,0 +1,51 @@
+(* Title: Pure/Thy/document_source.ML
+ Author: Makarius
+
+Document source for presentation.
+*)
+
+signature DOCUMENT_SOURCE =
+sig
+ val is_white: Token.T -> bool
+ val is_black: Token.T -> bool
+ val is_white_comment: Token.T -> bool
+ val is_black_comment: Token.T -> bool
+ val is_improper: Token.T -> bool
+ val improper: Token.T list parser
+ val improper_end: Token.T list parser
+ val blank_end: Token.T list parser
+ val tag: string parser
+ val tags: string list parser
+end;
+
+structure Document_Source: DOCUMENT_SOURCE =
+struct
+
+(* white space and comments *)
+
+(*NB: arranging white space around command spans is a black art*)
+
+val is_white = Token.is_space orf Token.is_informal_comment;
+val is_black = not o is_white;
+
+val is_white_comment = Token.is_informal_comment;
+val is_black_comment = Token.is_formal_comment;
+
+
+val space_proper =
+ Scan.one Token.is_blank -- Scan.many is_white_comment -- Scan.one is_black;
+
+val is_improper = not o (is_black orf Token.is_begin_ignore orf Token.is_end_ignore);
+val improper = Scan.many is_improper;
+val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
+val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank));
+
+
+(* tags *)
+
+val tag_name = Parse.group (fn () => "document tag name") (Parse.short_ident || Parse.string);
+
+val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (tag_name --| blank_end);
+val tags = Scan.repeat tag;
+
+end;
--- a/src/Pure/Thy/thy_header.ML Thu Mar 07 16:59:12 2019 +0000
+++ b/src/Pure/Thy/thy_header.ML Fri Mar 08 17:05:23 2019 +0100
@@ -137,7 +137,7 @@
val keyword_spec =
Parse.group (fn () => "outer syntax keyword specification")
- (Parse.name -- opt_files -- Parse.tags);
+ (Parse.name -- opt_files -- Document_Source.tags);
val keyword_decl =
Scan.repeat1 Parse.string_position --
@@ -175,10 +175,10 @@
Parse.command_name textN ||
Parse.command_name txtN ||
Parse.command_name text_rawN) --
- Parse.tags -- Parse.!!! Parse.document_source;
+ Document_Source.tags -- Parse.!!! Parse.document_source;
val parse_header =
- (Scan.repeat heading -- Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
+ (Scan.repeat heading -- Parse.command_name theoryN -- Document_Source.tags) |-- Parse.!!! args;
fun read_tokens pos toks =
filter Token.is_proper toks
--- a/src/Pure/Thy/thy_output.ML Thu Mar 07 16:59:12 2019 +0000
+++ b/src/Pure/Thy/thy_output.ML Fri Mar 08 17:05:23 2019 +0100
@@ -170,15 +170,6 @@
(** present theory source **)
-(*NB: arranging white space around command spans is a black art*)
-
-val is_white = Token.is_space orf Token.is_informal_comment;
-val is_black = not o is_white;
-
-val is_white_comment = Token.is_informal_comment;
-val is_black_comment = Token.is_formal_comment;
-
-
(* presentation tokens *)
datatype token =
@@ -191,8 +182,8 @@
fun basic_token pred (Basic_Token tok) = pred tok
| basic_token _ _ = false;
-val white_token = basic_token is_white;
-val white_comment_token = basic_token is_white_comment;
+val white_token = basic_token Document_Source.is_white;
+val white_comment_token = basic_token Document_Source.is_white_comment;
val blank_token = basic_token Token.is_blank;
val newline_token = basic_token Token.is_newline;
@@ -348,14 +339,6 @@
val markup_true = "\\isamarkuptrue%\n";
val markup_false = "\\isamarkupfalse%\n";
-val space_proper =
- Scan.one Token.is_blank -- Scan.many is_white_comment -- Scan.one is_black;
-
-val is_improper = not o (is_black orf Token.is_begin_ignore orf Token.is_end_ignore);
-val improper = Scan.many is_improper;
-val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
-val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank));
-
val opt_newline = Scan.option (Scan.one Token.is_newline);
val ignore =
@@ -365,11 +348,10 @@
(if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline)
>> pair (d - 1));
-val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end);
-
val locale =
- Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
- Parse.!!! (improper |-- Parse.name --| (improper -- Parse.$$$ ")")));
+ Scan.option ((Parse.$$$ "(" -- Document_Source.improper -- Parse.$$$ "in") |--
+ Parse.!!!
+ (Document_Source.improper |-- Parse.name --| (Document_Source.improper -- Parse.$$$ ")")));
in
@@ -386,25 +368,26 @@
>> (fn d => (NONE, (Ignore_Token, ("", d))));
fun markup pred mk flag = Scan.peek (fn d =>
- improper |--
+ Document_Source.improper |--
Parse.position (Scan.one (fn tok =>
Token.is_command tok andalso pred keywords (Token.content_of tok))) --
- Scan.repeat tag --
- Parse.!!!! ((improper -- locale -- improper) |-- Parse.document_source --| improper_end)
- >> (fn (((tok, pos'), tags), source) =>
- let val name = Token.content_of tok
- in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end));
+ Scan.repeat Document_Source.tag --
+ Parse.!!!! ((Document_Source.improper -- locale -- Document_Source.improper) |--
+ Parse.document_source --| Document_Source.improper_end)
+ >> (fn (((tok, pos'), tags), source) =>
+ let val name = Token.content_of tok
+ in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end));
val command = Scan.peek (fn d =>
- Scan.optional (Scan.one Token.is_command_modifier ::: improper) [] --
- Scan.one Token.is_command -- Scan.repeat tag
+ Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] --
+ Scan.one Token.is_command -- Document_Source.tags
>> (fn ((cmd_mod, cmd), tags) =>
map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
[(SOME (Token.content_of cmd, Token.pos_of cmd, tags),
(Basic_Token cmd, (markup_false, d)))]));
val cmt = Scan.peek (fn d =>
- Scan.one is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
+ Scan.one Document_Source.is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
val other = Scan.peek (fn d =>
Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));