document markers are formal comments, and may thus occur anywhere in the command-span;
authorwenzelm
Sun Mar 10 21:12:29 2019 +0100 (6 weeks ago ago)
changeset 70072def3ec9cdb7e
parent 70071 cb643a1a5313
child 70073 f752f3993db8
document markers are formal comments, and may thus occur anywhere in the command-span;
clarified Outer_Syntax.parse_span, Outer_Syntax.parse_text wrt. span structure;
tuned signature;
etc/symbols
src/Pure/General/antiquote.ML
src/Pure/General/comment.ML
src/Pure/General/comment.scala
src/Pure/General/symbol.ML
src/Pure/General/symbol.scala
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/parse.ML
src/Pure/Isar/parse.scala
src/Pure/Isar/token.ML
src/Pure/Isar/token.scala
src/Pure/ML/ml_lex.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/command.scala
src/Pure/Pure.thy
src/Pure/Syntax/lexicon.ML
src/Pure/Thy/document_marker.ML
src/Pure/Thy/document_source.ML
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_output.ML
src/Pure/Tools/rail.ML
     1.1 --- a/etc/symbols	Sun Mar 10 15:31:24 2019 +0100
     1.2 +++ b/etc/symbols	Sun Mar 10 21:12:29 2019 +0100
     1.3 @@ -359,9 +359,9 @@
     1.4  \<hole>                 code: 0x002311
     1.5  \<newline>              code: 0x0023ce
     1.6  \<comment>              code: 0x002015  group: document  argument: space_cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
     1.7 -\<marker>               code: 0x002710  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
     1.8  \<^cancel>              code: 0x002326  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
     1.9  \<^latex>                               group: document  argument: cartouche
    1.10 +\<^marker>              code: 0x002710  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
    1.11  \<open>                 code: 0x002039  group: punctuation  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: <<
    1.12  \<close>                code: 0x00203a  group: punctuation  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: >>
    1.13  \<^here>                code: 0x002302  font: Isabelle␣DejaVu␣Sans␣Mono
     2.1 --- a/src/Pure/General/antiquote.ML	Sun Mar 10 15:31:24 2019 +0100
     2.2 +++ b/src/Pure/General/antiquote.ML	Sun Mar 10 21:12:29 2019 +0100
     2.3 @@ -122,12 +122,12 @@
     2.4    scan_nl || Scan.repeats1 scan_plain_txt @@@ scan_nl_opt;
     2.5  
     2.6  val scan_text_comments =
     2.7 -  scan_nl || Scan.repeats1 (Comment.scan >> #2 || scan_plain_txt) @@@ scan_nl_opt;
     2.8 +  scan_nl || Scan.repeats1 (Comment.scan_inner >> #2 || scan_plain_txt) @@@ scan_nl_opt;
     2.9  
    2.10  val scan_antiq_body =
    2.11    Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
    2.12    Symbol_Pos.scan_cartouche err_prefix ||
    2.13 -  Comment.scan --
    2.14 +  Comment.scan_inner --
    2.15      Symbol_Pos.!!! (fn () => err_prefix ^ "bad formal comment in antiquote body") Scan.fail
    2.16      >> K [] ||
    2.17    Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single;
     3.1 --- a/src/Pure/General/comment.ML	Sun Mar 10 15:31:24 2019 +0100
     3.2 +++ b/src/Pure/General/comment.ML	Sun Mar 10 21:12:29 2019 +0100
     3.3 @@ -6,13 +6,15 @@
     3.4  
     3.5  signature COMMENT =
     3.6  sig
     3.7 -  datatype kind = Comment | Cancel | Latex
     3.8 +  datatype kind = Comment | Cancel | Latex | Marker
     3.9    val markups: kind -> Markup.T list
    3.10    val is_symbol: Symbol.symbol -> bool
    3.11    val scan_comment: (kind * Symbol_Pos.T list) scanner
    3.12    val scan_cancel: (kind * Symbol_Pos.T list) scanner
    3.13    val scan_latex: (kind * Symbol_Pos.T list) scanner
    3.14 -  val scan: (kind * Symbol_Pos.T list) scanner
    3.15 +  val scan_marker: (kind * Symbol_Pos.T list) scanner
    3.16 +  val scan_inner: (kind * Symbol_Pos.T list) scanner
    3.17 +  val scan_outer: (kind * Symbol_Pos.T list) scanner
    3.18    val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list
    3.19  end;
    3.20  
    3.21 @@ -21,7 +23,7 @@
    3.22  
    3.23  (* kinds *)
    3.24  
    3.25 -datatype kind = Comment | Cancel | Latex;
    3.26 +datatype kind = Comment | Cancel | Latex | Marker;
    3.27  
    3.28  val kinds =
    3.29    [(Comment,
    3.30 @@ -32,7 +34,10 @@
    3.31        markups = [Markup.language_text true]}),
    3.32     (Latex,
    3.33       {symbol = Symbol.latex, blanks = false,
    3.34 -      markups = [Markup.language_latex true, Markup.no_words]})];
    3.35 +      markups = [Markup.language_latex true, Markup.no_words]}),
    3.36 +   (Marker,
    3.37 +     {symbol = Symbol.marker, blanks = false,
    3.38 +      markups = [Markup.language_document_marker]})];
    3.39  
    3.40  val get_kind = the o AList.lookup (op =) kinds;
    3.41  val print_kind = quote o #symbol o get_kind;
    3.42 @@ -69,7 +74,10 @@
    3.43  val scan_comment = scan_strict Comment;
    3.44  val scan_cancel = scan_strict Cancel;
    3.45  val scan_latex = scan_strict Latex;
    3.46 -val scan = scan_comment || scan_cancel || scan_latex;
    3.47 +val scan_marker = scan_strict Marker;
    3.48 +
    3.49 +val scan_inner = scan_comment || scan_cancel || scan_latex;
    3.50 +val scan_outer = scan_inner || scan_marker;
    3.51  
    3.52  val scan_body =
    3.53    Scan.many1 (fn (s, _) => not (is_symbol s) andalso Symbol.not_eof s) >> pair NONE ||
     4.1 --- a/src/Pure/General/comment.scala	Sun Mar 10 15:31:24 2019 +0100
     4.2 +++ b/src/Pure/General/comment.scala	Sun Mar 10 21:12:29 2019 +0100
     4.3 @@ -14,12 +14,14 @@
     4.4      val COMMENT = Value("formal comment")
     4.5      val CANCEL = Value("canceled text")
     4.6      val LATEX = Value("embedded LaTeX")
     4.7 +    val MARKER = Value("document marker")
     4.8    }
     4.9  
    4.10    lazy val symbols: Set[Symbol.Symbol] =
    4.11      Set(Symbol.comment, Symbol.comment_decoded,
    4.12        Symbol.cancel, Symbol.cancel_decoded,
    4.13 -      Symbol.latex, Symbol.latex_decoded)
    4.14 +      Symbol.latex, Symbol.latex_decoded,
    4.15 +      Symbol.marker, Symbol.marker_decoded)
    4.16  
    4.17    lazy val symbols_blanks: Set[Symbol.Symbol] =
    4.18      Set(Symbol.comment, Symbol.comment_decoded)
     5.1 --- a/src/Pure/General/symbol.ML	Sun Mar 10 15:31:24 2019 +0100
     5.2 +++ b/src/Pure/General/symbol.ML	Sun Mar 10 21:12:29 2019 +0100
     5.3 @@ -18,6 +18,7 @@
     5.4    val comment: symbol
     5.5    val cancel: symbol
     5.6    val latex: symbol
     5.7 +  val marker: symbol
     5.8    val is_char: symbol -> bool
     5.9    val is_utf8: symbol -> bool
    5.10    val is_symbolic: symbol -> bool
    5.11 @@ -120,6 +121,7 @@
    5.12  val comment = "\<comment>";
    5.13  val cancel = "\<^cancel>";
    5.14  val latex = "\<^latex>";
    5.15 +val marker = "\<^marker>";
    5.16  
    5.17  fun is_char s = size s = 1;
    5.18  
     6.1 --- a/src/Pure/General/symbol.scala	Sun Mar 10 15:31:24 2019 +0100
     6.2 +++ b/src/Pure/General/symbol.scala	Sun Mar 10 21:12:29 2019 +0100
     6.3 @@ -493,10 +493,10 @@
     6.4      /* misc symbols */
     6.5  
     6.6      val newline_decoded = decode(newline)
     6.7 -    val marker_decoded = decode(marker)
     6.8      val comment_decoded = decode(comment)
     6.9      val cancel_decoded = decode(cancel)
    6.10      val latex_decoded = decode(latex)
    6.11 +    val marker_decoded = decode(marker)
    6.12      val open_decoded = decode(open)
    6.13      val close_decoded = decode(close)
    6.14  
    6.15 @@ -579,23 +579,17 @@
    6.16      else str
    6.17  
    6.18  
    6.19 -  /* marker */
    6.20 -
    6.21 -  val marker: Symbol = "\\<marker>"
    6.22 -  def marker_decoded: Symbol = symbols.marker_decoded
    6.23 -
    6.24 -  lazy val is_marker: Set[Symbol] = Set(marker, marker_decoded)
    6.25 -
    6.26 -
    6.27    /* formal comments */
    6.28  
    6.29    val comment: Symbol = "\\<comment>"
    6.30    val cancel: Symbol = "\\<^cancel>"
    6.31    val latex: Symbol = "\\<^latex>"
    6.32 +  val marker: Symbol = "\\<^marker>"
    6.33  
    6.34    def comment_decoded: Symbol = symbols.comment_decoded
    6.35    def cancel_decoded: Symbol = symbols.cancel_decoded
    6.36    def latex_decoded: Symbol = symbols.latex_decoded
    6.37 +  def marker_decoded: Symbol = symbols.marker_decoded
    6.38  
    6.39  
    6.40    /* cartouches */
     7.1 --- a/src/Pure/Isar/outer_syntax.ML	Sun Mar 10 15:31:24 2019 +0100
     7.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sun Mar 10 21:12:29 2019 +0100
     7.3 @@ -22,10 +22,10 @@
     7.4    val local_theory_to_proof: command_keyword -> string ->
     7.5      (local_theory -> Proof.state) parser -> unit
     7.6    val bootstrap: bool Config.T
     7.7 -  val parse_tokens: theory -> Token.T list -> Toplevel.transition list
     7.8 -  val parse: theory -> Position.T -> string -> Toplevel.transition list
     7.9    val parse_spans: Token.T list -> Command_Span.span list
    7.10    val make_span: Token.T list -> Command_Span.span
    7.11 +  val parse_span: theory -> (unit -> theory) -> Token.T list -> Toplevel.transition
    7.12 +  val parse_text: theory -> (unit -> theory) -> Position.T -> string -> Toplevel.transition list
    7.13    val command_reports: theory -> Token.T -> Position.report_text list
    7.14    val check_command: Proof.context -> command_keyword -> string
    7.15  end;
    7.16 @@ -172,60 +172,6 @@
    7.17  
    7.18  (** toplevel parsing **)
    7.19  
    7.20 -(* parse commands *)
    7.21 -
    7.22 -val bootstrap = Config.declare_bool ("Outer_Syntax.bootstrap", \<^here>) (K true);
    7.23 -
    7.24 -local
    7.25 -
    7.26 -val before_command =
    7.27 -  Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false));
    7.28 -
    7.29 -fun parse_command thy =
    7.30 -  Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) =>
    7.31 -    let
    7.32 -      val keywords = Thy_Header.get_keywords thy;
    7.33 -      val tr0 =
    7.34 -        Toplevel.empty
    7.35 -        |> Toplevel.name name
    7.36 -        |> Toplevel.position pos
    7.37 -        |> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open
    7.38 -        |> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close;
    7.39 -      val command_marker =
    7.40 -        Parse.command |-- Document_Source.annotation >> (fn markers => Toplevel.markers markers tr0);
    7.41 -    in
    7.42 -      (case lookup_commands thy name of
    7.43 -        SOME (Command {command_parser = Parser parse, ...}) =>
    7.44 -          Parse.!!! (command_marker -- parse) >> (op |>)
    7.45 -      | SOME (Command {command_parser = Restricted_Parser parse, ...}) =>
    7.46 -          before_command :|-- (fn restricted =>
    7.47 -            Parse.!!! (command_marker -- parse restricted)) >> (op |>)
    7.48 -      | NONE =>
    7.49 -          Scan.fail_with (fn _ => fn _ =>
    7.50 -            let
    7.51 -              val msg =
    7.52 -                if Config.get_global thy bootstrap
    7.53 -                then "missing theory context for command "
    7.54 -                else "undefined command ";
    7.55 -            in msg ^ quote (Markup.markup Markup.keyword1 name) end))
    7.56 -    end);
    7.57 -
    7.58 -in
    7.59 -
    7.60 -fun parse_tokens thy =
    7.61 -  filter Token.is_proper
    7.62 -  #> Source.of_list
    7.63 -  #> Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy) xs))
    7.64 -  #> Source.exhaust;
    7.65 -
    7.66 -fun parse thy pos text =
    7.67 -  Symbol_Pos.explode (text, pos)
    7.68 -  |> Token.tokenize (Thy_Header.get_keywords thy) {strict = false}
    7.69 -  |> parse_tokens thy;
    7.70 -
    7.71 -end;
    7.72 -
    7.73 -
    7.74  (* parse spans *)
    7.75  
    7.76  local
    7.77 @@ -267,6 +213,75 @@
    7.78    | _ => Command_Span.Span (Command_Span.Malformed_Span, toks));
    7.79  
    7.80  
    7.81 +(* parse commands *)
    7.82 +
    7.83 +val bootstrap = Config.declare_bool ("Outer_Syntax.bootstrap", \<^here>) (K true);
    7.84 +
    7.85 +local
    7.86 +
    7.87 +val before_command =
    7.88 +  Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false));
    7.89 +
    7.90 +fun parse_command thy markers =
    7.91 +  Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) =>
    7.92 +    let
    7.93 +      val keywords = Thy_Header.get_keywords thy;
    7.94 +      val tr0 =
    7.95 +        Toplevel.empty
    7.96 +        |> Toplevel.name name
    7.97 +        |> Toplevel.position pos
    7.98 +        |> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open
    7.99 +        |> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close;
   7.100 +      val command_markers =
   7.101 +        Parse.command |-- Document_Source.tags >>
   7.102 +          (fn tags => Toplevel.markers (map Document_Marker.legacy_tag tags @ markers) tr0);
   7.103 +    in
   7.104 +      (case lookup_commands thy name of
   7.105 +        SOME (Command {command_parser = Parser parse, ...}) =>
   7.106 +          Parse.!!! (command_markers -- parse) >> (op |>)
   7.107 +      | SOME (Command {command_parser = Restricted_Parser parse, ...}) =>
   7.108 +          before_command :|-- (fn restricted =>
   7.109 +            Parse.!!! (command_markers -- parse restricted)) >> (op |>)
   7.110 +      | NONE =>
   7.111 +          Scan.fail_with (fn _ => fn _ =>
   7.112 +            let
   7.113 +              val msg =
   7.114 +                if Config.get_global thy bootstrap
   7.115 +                then "missing theory context for command "
   7.116 +                else "undefined command ";
   7.117 +            in msg ^ quote (Markup.markup Markup.keyword1 name) end))
   7.118 +    end);
   7.119 +
   7.120 +in
   7.121 +
   7.122 +fun parse_span thy init span =
   7.123 +  let
   7.124 +    val range = Token.range_of span;
   7.125 +    val core_range = Token.core_range_of span;
   7.126 +
   7.127 +    val markers = map Token.input_of (filter Token.is_document_marker span);
   7.128 +    fun parse () =
   7.129 +      filter Token.is_proper span
   7.130 +      |> Source.of_list
   7.131 +      |> Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy markers) xs))
   7.132 +      |> Source.exhaust;
   7.133 +  in
   7.134 +    (case parse () of
   7.135 +      [tr] => Toplevel.modify_init init tr
   7.136 +    | [] => Toplevel.ignored (#1 range)
   7.137 +    | _ => Toplevel.malformed (#1 core_range) "Exactly one command expected")
   7.138 +    handle ERROR msg => Toplevel.malformed (#1 core_range) msg
   7.139 +  end;
   7.140 +
   7.141 +fun parse_text thy init pos text =
   7.142 +  Symbol_Pos.explode (text, pos)
   7.143 +  |> Token.tokenize (Thy_Header.get_keywords thy) {strict = false}
   7.144 +  |> parse_spans
   7.145 +  |> map (Command_Span.content #> parse_span thy init);
   7.146 +
   7.147 +end;
   7.148 +
   7.149 +
   7.150  (* check commands *)
   7.151  
   7.152  fun command_reports thy tok =
     8.1 --- a/src/Pure/Isar/parse.ML	Sun Mar 10 15:31:24 2019 +0100
     8.2 +++ b/src/Pure/Isar/parse.ML	Sun Mar 10 21:12:29 2019 +0100
     8.3 @@ -96,6 +96,7 @@
     8.4    val for_fixes: (binding * string option * mixfix) list parser
     8.5    val ML_source: Input.source parser
     8.6    val document_source: Input.source parser
     8.7 +  val document_marker: Input.source parser
     8.8    val const: string parser
     8.9    val term: string parser
    8.10    val prop: string parser
    8.11 @@ -390,6 +391,10 @@
    8.12  val ML_source = input (group (fn () => "ML source") text);
    8.13  val document_source = input (group (fn () => "document source") text);
    8.14  
    8.15 +val document_marker =
    8.16 +  group (fn () => "document marker")
    8.17 +    (RESET_VALUE (Scan.one Token.is_document_marker >> Token.input_of));
    8.18 +
    8.19  
    8.20  (* terms *)
    8.21  
     9.1 --- a/src/Pure/Isar/parse.scala	Sun Mar 10 15:31:24 2019 +0100
     9.2 +++ b/src/Pure/Isar/parse.scala	Sun Mar 10 21:12:29 2019 +0100
     9.3 @@ -83,10 +83,9 @@
     9.4      def tag: Parser[String] = $$$("%") ~> tag_name
     9.5      def tags: Parser[List[String]] = rep(tag)
     9.6  
     9.7 -    def marker: Parser[String] =
     9.8 -      ($$$(Symbol.marker) | $$$(Symbol.marker_decoded)) ~! embedded ^^ { case _ ~ x => x }
     9.9 +    def marker: Parser[String] = token("marker", _.is_marker) ^^ (_.content)
    9.10  
    9.11 -    def annotation: Parser[Unit] = rep(marker | tag) ^^ { case _ => () }
    9.12 +    def annotation: Parser[Unit] = rep(tag | marker) ^^ { case _ => () }
    9.13  
    9.14  
    9.15      /* wrappers */
    10.1 --- a/src/Pure/Isar/token.ML	Sun Mar 10 15:31:24 2019 +0100
    10.2 +++ b/src/Pure/Isar/token.ML	Sun Mar 10 21:12:29 2019 +0100
    10.3 @@ -30,7 +30,6 @@
    10.4      Declaration of declaration |
    10.5      Files of file Exn.result list
    10.6    val pos_of: T -> Position.T
    10.7 -  val range_of: T list -> Position.range
    10.8    val adjust_offsets: (int -> int option) -> T -> T
    10.9    val eof: T
   10.10    val is_eof: T -> bool
   10.11 @@ -46,6 +45,7 @@
   10.12    val is_comment: T -> bool
   10.13    val is_informal_comment: T -> bool
   10.14    val is_formal_comment: T -> bool
   10.15 +  val is_document_marker: T -> bool
   10.16    val is_ignored: T -> bool
   10.17    val is_begin_ignore: T -> bool
   10.18    val is_end_ignore: T -> bool
   10.19 @@ -53,6 +53,8 @@
   10.20    val is_space: T -> bool
   10.21    val is_blank: T -> bool
   10.22    val is_newline: T -> bool
   10.23 +  val range_of: T list -> Position.range
   10.24 +  val core_range_of: T list -> Position.range
   10.25    val content_of: T -> string
   10.26    val source_of: T -> string
   10.27    val input_of: T -> Input.source
   10.28 @@ -190,11 +192,6 @@
   10.29  fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
   10.30  fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos;
   10.31  
   10.32 -fun range_of (toks as tok :: _) =
   10.33 -      let val pos' = end_pos_of (List.last toks)
   10.34 -      in Position.range (pos_of tok, pos') end
   10.35 -  | range_of [] = Position.no_range;
   10.36 -
   10.37  fun adjust_offsets adjust (Token ((x, range), y, z)) =
   10.38    Token ((x, apply2 (Position.adjust_offsets adjust) range), y, z);
   10.39  
   10.40 @@ -245,6 +242,9 @@
   10.41  fun is_formal_comment (Token (_, (Comment (SOME _), _), _)) = true
   10.42    | is_formal_comment _ = false;
   10.43  
   10.44 +fun is_document_marker (Token (_, (Comment (SOME Comment.Marker), _), _)) = true
   10.45 +  | is_document_marker _ = false;
   10.46 +
   10.47  fun is_begin_ignore (Token (_, (Comment NONE, "<"), _)) = true
   10.48    | is_begin_ignore _ = false;
   10.49  
   10.50 @@ -267,6 +267,17 @@
   10.51    | is_newline _ = false;
   10.52  
   10.53  
   10.54 +(* range of tokens *)
   10.55 +
   10.56 +fun range_of (toks as tok :: _) =
   10.57 +      let val pos' = end_pos_of (List.last toks)
   10.58 +      in Position.range (pos_of tok, pos') end
   10.59 +  | range_of [] = Position.no_range;
   10.60 +
   10.61 +val core_range_of =
   10.62 +  drop_prefix is_ignored #> drop_suffix is_ignored #> range_of;
   10.63 +
   10.64 +
   10.65  (* token content *)
   10.66  
   10.67  fun content_of (Token (_, (_, x), _)) = x;
   10.68 @@ -636,7 +647,7 @@
   10.69      scan_verbatim >> token_range Verbatim ||
   10.70      scan_cartouche >> token_range Cartouche ||
   10.71      scan_comment >> token_range (Comment NONE) ||
   10.72 -    Comment.scan >> (fn (k, ss) => token (Comment (SOME k)) ss) ||
   10.73 +    Comment.scan_outer >> (fn (k, ss) => token (Comment (SOME k)) ss) ||
   10.74      scan_space >> token Space ||
   10.75      (Scan.max token_leq
   10.76        (Scan.max token_leq
    11.1 --- a/src/Pure/Isar/token.scala	Sun Mar 10 15:31:24 2019 +0100
    11.2 +++ b/src/Pure/Isar/token.scala	Sun Mar 10 21:12:29 2019 +0100
    11.3 @@ -304,6 +304,9 @@
    11.4    def is_space: Boolean = kind == Token.Kind.SPACE
    11.5    def is_informal_comment: Boolean = kind == Token.Kind.INFORMAL_COMMENT
    11.6    def is_formal_comment: Boolean = kind == Token.Kind.FORMAL_COMMENT
    11.7 +  def is_marker: Boolean =
    11.8 +    kind == Token.Kind.FORMAL_COMMENT &&
    11.9 +    (source.startsWith(Symbol.marker) || source.startsWith(Symbol.marker_decoded))
   11.10    def is_comment: Boolean = is_informal_comment || is_formal_comment
   11.11    def is_ignored: Boolean = is_space || is_informal_comment
   11.12    def is_proper: Boolean = !is_space && !is_comment
    12.1 --- a/src/Pure/ML/ml_lex.ML	Sun Mar 10 15:31:24 2019 +0100
    12.2 +++ b/src/Pure/ML/ml_lex.ML	Sun Mar 10 21:12:29 2019 +0100
    12.3 @@ -312,7 +312,7 @@
    12.4  val scan_sml_antiq = scan_sml >> Antiquote.Text;
    12.5  
    12.6  val scan_ml_antiq =
    12.7 -  Comment.scan >> (fn (kind, ss) => Antiquote.Text (token (Comment (SOME kind)) ss)) ||
    12.8 +  Comment.scan_inner >> (fn (kind, ss) => Antiquote.Text (token (Comment (SOME kind)) ss)) ||
    12.9    Antiquote.scan_control >> Antiquote.Control ||
   12.10    Antiquote.scan_antiq >> Antiquote.Antiq ||
   12.11    scan_rat_antiq >> Antiquote.Antiq ||
    13.1 --- a/src/Pure/PIDE/command.ML	Sun Mar 10 15:31:24 2019 +0100
    13.2 +++ b/src/Pure/PIDE/command.ML	Sun Mar 10 21:12:29 2019 +0100
    13.3 @@ -155,12 +155,7 @@
    13.4          Position.here_list verbatim);
    13.5    in
    13.6      if exists #1 token_reports then Toplevel.malformed pos "Malformed command syntax"
    13.7 -    else
    13.8 -      (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs_info span) of
    13.9 -        [tr] => Toplevel.modify_init init tr
   13.10 -      | [] => Toplevel.ignored (#1 (Token.range_of span))
   13.11 -      | _ => Toplevel.malformed (#1 core_range) "Exactly one command expected")
   13.12 -      handle ERROR msg => Toplevel.malformed (#1 core_range) msg
   13.13 +    else Outer_Syntax.parse_span thy init (resolve_files keywords master_dir blobs_info span)
   13.14    end;
   13.15  
   13.16  end;
    14.1 --- a/src/Pure/PIDE/command.scala	Sun Mar 10 15:31:24 2019 +0100
    14.2 +++ b/src/Pure/PIDE/command.scala	Sun Mar 10 21:12:29 2019 +0100
    14.3 @@ -475,7 +475,6 @@
    14.4        toks match {
    14.5          case (t1, i1) :: (t2, i2) :: rest =>
    14.6            if (t1.is_keyword && t1.source == "%" && t2.is_name) clean(rest)
    14.7 -          else if (t1.is_keyword && Symbol.is_marker(t1.source) && t2.is_embedded) clean(rest)
    14.8            else (t1, i1) :: clean((t2, i2) :: rest)
    14.9          case _ => toks
   14.10        }
    15.1 --- a/src/Pure/Pure.thy	Sun Mar 10 15:31:24 2019 +0100
    15.2 +++ b/src/Pure/Pure.thy	Sun Mar 10 21:12:29 2019 +0100
    15.3 @@ -7,7 +7,7 @@
    15.4  theory Pure
    15.5  keywords
    15.6      "!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
    15.7 -    "\<marker>" "\<subseteq>" "]" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output"
    15.8 +    "\<subseteq>" "]" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output"
    15.9      "overloaded" "pervasive" "premises" "structure" "unchecked"
   15.10    and "private" "qualified" :: before_command
   15.11    and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites"
    16.1 --- a/src/Pure/Syntax/lexicon.ML	Sun Mar 10 15:31:24 2019 +0100
    16.2 +++ b/src/Pure/Syntax/lexicon.ML	Sun Mar 10 21:12:29 2019 +0100
    16.3 @@ -301,7 +301,7 @@
    16.4  
    16.5      val scan =
    16.6        Symbol_Pos.scan_cartouche err_prefix >> token Cartouche ||
    16.7 -      Comment.scan >> (fn (kind, ss) => token (Comment kind) ss) ||
    16.8 +      Comment.scan_inner >> (fn (kind, ss) => token (Comment kind) ss) ||
    16.9        Scan.max token_leq scan_lit scan_val ||
   16.10        scan_string >> token String ||
   16.11        scan_str >> token Str ||
    17.1 --- a/src/Pure/Thy/document_marker.ML	Sun Mar 10 15:31:24 2019 +0100
    17.2 +++ b/src/Pure/Thy/document_marker.ML	Sun Mar 10 21:12:29 2019 +0100
    17.3 @@ -10,6 +10,7 @@
    17.4    val setup: binding -> 'a context_parser -> ('a -> marker) -> theory -> theory
    17.5    val setup0: binding -> 'a parser -> ('a -> marker) -> theory -> theory
    17.6    val evaluate: Input.source -> marker
    17.7 +  val legacy_tag: string -> Input.source
    17.8  end;
    17.9  
   17.10  structure Document_Marker: DOCUMENT_MARKER =
   17.11 @@ -47,14 +48,14 @@
   17.12  
   17.13  fun evaluate input ctxt =
   17.14    let
   17.15 -    val pos = Input.pos_of input;
   17.16 -    val _ = Context_Position.report ctxt pos Markup.language_document_marker;
   17.17 -
   17.18 -    val syms = Input.source_explode input;
   17.19 +    val body =
   17.20 +      Input.source_explode input
   17.21 +      |> drop_prefix (fn (s, _) => s = Symbol.marker)
   17.22 +      |> Symbol_Pos.cartouche_content;
   17.23      val markers =
   17.24 -      (case Token.read_body (Thy_Header.get_keywords' ctxt) (Parse.list parse_marker) syms of
   17.25 +      (case Token.read_body (Thy_Header.get_keywords' ctxt) (Parse.list parse_marker) body of
   17.26          SOME res => res
   17.27 -      | NONE => error ("Bad input" ^ Position.here pos));
   17.28 +      | NONE => error ("Bad input" ^ Position.here (Input.pos_of input)));
   17.29    in fold (fn src => #2 (check ctxt (Token.name_of_src src)) src) markers ctxt end;
   17.30  
   17.31  
   17.32 @@ -77,4 +78,7 @@
   17.33            val _ = Context_Position.report ctxt pos Markup.words;
   17.34          in meta_data Markup.meta_description arg ctxt end));
   17.35  
   17.36 +fun legacy_tag name =
   17.37 +  Input.string (cartouche ("tag " ^ Symbol_Pos.quote_string_qq name));
   17.38 +
   17.39  end;
    18.1 --- a/src/Pure/Thy/document_source.ML	Sun Mar 10 15:31:24 2019 +0100
    18.2 +++ b/src/Pure/Thy/document_source.ML	Sun Mar 10 21:12:29 2019 +0100
    18.3 @@ -17,7 +17,7 @@
    18.4    val get_tags: Proof.context -> string list
    18.5    val update_tags: string -> Proof.context -> Proof.context
    18.6    val tags: string list parser
    18.7 -  val annotation: Input.source list parser
    18.8 +  val annotation: unit parser
    18.9  end;
   18.10  
   18.11  structure Document_Source: DOCUMENT_SOURCE =
   18.12 @@ -62,13 +62,8 @@
   18.13  
   18.14  (* semantic markers (operation on presentation context) *)
   18.15  
   18.16 -val marker =
   18.17 -  (improper -- Parse.$$$ "\<marker>" -- improper) |--
   18.18 -    Parse.!!! (Parse.group (fn () => "document marker") (Parse.input Parse.embedded) --| blank_end);
   18.19 +val marker = improper |-- Parse.document_marker --| blank_end;
   18.20  
   18.21 -val tag_marker =  (*emulation of old-style tags*)
   18.22 -  tag >> (fn name => Input.string ("tag " ^ Symbol_Pos.quote_string_qq name));
   18.23 -
   18.24 -val annotation = Scan.repeat (marker || tag_marker);
   18.25 +val annotation = Scan.repeat (tag >> K () || marker >> K ()) >> K ();
   18.26  
   18.27  end;
    19.1 --- a/src/Pure/Thy/thy_header.ML	Sun Mar 10 15:31:24 2019 +0100
    19.2 +++ b/src/Pure/Thy/thy_header.ML	Sun Mar 10 21:12:29 2019 +0100
    19.3 @@ -175,10 +175,10 @@
    19.4      Parse.command_name textN ||
    19.5      Parse.command_name txtN ||
    19.6      Parse.command_name text_rawN) --
    19.7 -  Document_Source.annotation -- Parse.!!! Parse.document_source;
    19.8 +  (Document_Source.annotation |-- Parse.!!! Parse.document_source);
    19.9  
   19.10  val parse_header =
   19.11 -  (Scan.repeat heading -- Parse.command_name theoryN -- Document_Source.annotation)
   19.12 +  (Scan.repeat heading -- Parse.command_name theoryN --| Document_Source.annotation)
   19.13      |-- Parse.!!! args;
   19.14  
   19.15  fun read_tokens pos toks =
    20.1 --- a/src/Pure/Thy/thy_info.ML	Sun Mar 10 15:31:24 2019 +0100
    20.2 +++ b/src/Pure/Thy/thy_info.ML	Sun Mar 10 21:12:29 2019 +0100
    20.3 @@ -451,9 +451,7 @@
    20.4  
    20.5  fun script_thy pos txt thy =
    20.6    let
    20.7 -    val trs =
    20.8 -      Outer_Syntax.parse thy pos txt
    20.9 -      |> map (Toplevel.modify_init (K thy));
   20.10 +    val trs = Outer_Syntax.parse_text thy (K thy) pos txt;
   20.11      val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
   20.12      val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ());
   20.13    in Toplevel.end_theory end_pos end_state end;
    21.1 --- a/src/Pure/Thy/thy_output.ML	Sun Mar 10 15:31:24 2019 +0100
    21.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Mar 10 21:12:29 2019 +0100
    21.3 @@ -61,8 +61,8 @@
    21.4        Symbol_Pos.cartouche_content syms
    21.5        |> output_symbols
    21.6        |> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
    21.7 -  | Comment.Latex =>
    21.8 -      [Latex.symbols (Symbol_Pos.cartouche_content syms)])
    21.9 +  | Comment.Latex => [Latex.symbols (Symbol_Pos.cartouche_content syms)]
   21.10 +  | Comment.Marker => [])
   21.11  and output_comment_document ctxt (comment, syms) =
   21.12    (case comment of
   21.13      SOME kind => output_comment ctxt (kind, syms)
   21.14 @@ -139,6 +139,7 @@
   21.15    in
   21.16      (case Token.kind_of tok of
   21.17        Token.Comment NONE => []
   21.18 +    | Token.Comment (SOME Comment.Marker) => []
   21.19      | Token.Command => output false "\\isacommand{" "}"
   21.20      | Token.Keyword =>
   21.21          if Symbol.is_ascii_identifier (Token.content_of tok)
    22.1 --- a/src/Pure/Tools/rail.ML	Sun Mar 10 15:31:24 2019 +0100
    22.2 +++ b/src/Pure/Tools/rail.ML	Sun Mar 10 21:12:29 2019 +0100
    22.3 @@ -118,7 +118,7 @@
    22.4  
    22.5  val scan_token =
    22.6    scan_space >> token Space ||
    22.7 -  Comment.scan >> (fn (kind, ss) => token (Comment kind) ss)||
    22.8 +  Comment.scan_inner >> (fn (kind, ss) => token (Comment kind) ss) ||
    22.9    Antiquote.scan_antiq >> antiq_token ||
   22.10    scan_keyword >> (token Keyword o single) ||
   22.11    Lexicon.scan_id >> token Ident ||