# HG changeset patch
# User wenzelm
# Date 1552061123 -3600
# Node ID b49bd228ac8a79f8f5a367069bdec70595a2909d
# Parent  03bc14eab432dbdd11c3245ed45e8dcc3391064a
clarified modules;
uniform "tag" parser;

diff -r 03bc14eab432 -r b49bd228ac8a src/Pure/Isar/outer_syntax.ML
--- 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
diff -r 03bc14eab432 -r b49bd228ac8a src/Pure/Isar/parse.ML
--- 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;
 
diff -r 03bc14eab432 -r b49bd228ac8a src/Pure/ROOT.ML
--- 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*)
diff -r 03bc14eab432 -r b49bd228ac8a src/Pure/Thy/document_source.ML
--- /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;
diff -r 03bc14eab432 -r b49bd228ac8a src/Pure/Thy/thy_header.ML
--- 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
diff -r 03bc14eab432 -r b49bd228ac8a src/Pure/Thy/thy_output.ML
--- 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)))));