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;
--- a/etc/symbols Sun Mar 10 15:31:24 2019 +0100
+++ b/etc/symbols Sun Mar 10 21:12:29 2019 +0100
@@ -359,9 +359,9 @@
\<hole> code: 0x002311
\<newline> code: 0x0023ce
\<comment> code: 0x002015 group: document argument: space_cartouche font: Isabelle␣DejaVu␣Sans␣Mono
-\<marker> code: 0x002710 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
\<^cancel> code: 0x002326 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
\<^latex> group: document argument: cartouche
+\<^marker> code: 0x002710 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
\<open> code: 0x002039 group: punctuation font: Isabelle␣DejaVu␣Sans␣Mono abbrev: <<
\<close> code: 0x00203a group: punctuation font: Isabelle␣DejaVu␣Sans␣Mono abbrev: >>
\<^here> code: 0x002302 font: Isabelle␣DejaVu␣Sans␣Mono
--- a/src/Pure/General/antiquote.ML Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/General/antiquote.ML Sun Mar 10 21:12:29 2019 +0100
@@ -122,12 +122,12 @@
scan_nl || Scan.repeats1 scan_plain_txt @@@ scan_nl_opt;
val scan_text_comments =
- scan_nl || Scan.repeats1 (Comment.scan >> #2 || scan_plain_txt) @@@ scan_nl_opt;
+ scan_nl || Scan.repeats1 (Comment.scan_inner >> #2 || scan_plain_txt) @@@ scan_nl_opt;
val scan_antiq_body =
Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
Symbol_Pos.scan_cartouche err_prefix ||
- Comment.scan --
+ Comment.scan_inner --
Symbol_Pos.!!! (fn () => err_prefix ^ "bad formal comment in antiquote body") Scan.fail
>> K [] ||
Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single;
--- a/src/Pure/General/comment.ML Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/General/comment.ML Sun Mar 10 21:12:29 2019 +0100
@@ -6,13 +6,15 @@
signature COMMENT =
sig
- datatype kind = Comment | Cancel | Latex
+ datatype kind = Comment | Cancel | Latex | Marker
val markups: kind -> Markup.T list
val is_symbol: Symbol.symbol -> bool
val scan_comment: (kind * Symbol_Pos.T list) scanner
val scan_cancel: (kind * Symbol_Pos.T list) scanner
val scan_latex: (kind * Symbol_Pos.T list) scanner
- val scan: (kind * Symbol_Pos.T list) scanner
+ val scan_marker: (kind * Symbol_Pos.T list) scanner
+ val scan_inner: (kind * Symbol_Pos.T list) scanner
+ val scan_outer: (kind * Symbol_Pos.T list) scanner
val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list
end;
@@ -21,7 +23,7 @@
(* kinds *)
-datatype kind = Comment | Cancel | Latex;
+datatype kind = Comment | Cancel | Latex | Marker;
val kinds =
[(Comment,
@@ -32,7 +34,10 @@
markups = [Markup.language_text true]}),
(Latex,
{symbol = Symbol.latex, blanks = false,
- markups = [Markup.language_latex true, Markup.no_words]})];
+ markups = [Markup.language_latex true, Markup.no_words]}),
+ (Marker,
+ {symbol = Symbol.marker, blanks = false,
+ markups = [Markup.language_document_marker]})];
val get_kind = the o AList.lookup (op =) kinds;
val print_kind = quote o #symbol o get_kind;
@@ -69,7 +74,10 @@
val scan_comment = scan_strict Comment;
val scan_cancel = scan_strict Cancel;
val scan_latex = scan_strict Latex;
-val scan = scan_comment || scan_cancel || scan_latex;
+val scan_marker = scan_strict Marker;
+
+val scan_inner = scan_comment || scan_cancel || scan_latex;
+val scan_outer = scan_inner || scan_marker;
val scan_body =
Scan.many1 (fn (s, _) => not (is_symbol s) andalso Symbol.not_eof s) >> pair NONE ||
--- a/src/Pure/General/comment.scala Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/General/comment.scala Sun Mar 10 21:12:29 2019 +0100
@@ -14,12 +14,14 @@
val COMMENT = Value("formal comment")
val CANCEL = Value("canceled text")
val LATEX = Value("embedded LaTeX")
+ val MARKER = Value("document marker")
}
lazy val symbols: Set[Symbol.Symbol] =
Set(Symbol.comment, Symbol.comment_decoded,
Symbol.cancel, Symbol.cancel_decoded,
- Symbol.latex, Symbol.latex_decoded)
+ Symbol.latex, Symbol.latex_decoded,
+ Symbol.marker, Symbol.marker_decoded)
lazy val symbols_blanks: Set[Symbol.Symbol] =
Set(Symbol.comment, Symbol.comment_decoded)
--- a/src/Pure/General/symbol.ML Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/General/symbol.ML Sun Mar 10 21:12:29 2019 +0100
@@ -18,6 +18,7 @@
val comment: symbol
val cancel: symbol
val latex: symbol
+ val marker: symbol
val is_char: symbol -> bool
val is_utf8: symbol -> bool
val is_symbolic: symbol -> bool
@@ -120,6 +121,7 @@
val comment = "\<comment>";
val cancel = "\<^cancel>";
val latex = "\<^latex>";
+val marker = "\<^marker>";
fun is_char s = size s = 1;
--- a/src/Pure/General/symbol.scala Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/General/symbol.scala Sun Mar 10 21:12:29 2019 +0100
@@ -493,10 +493,10 @@
/* misc symbols */
val newline_decoded = decode(newline)
- val marker_decoded = decode(marker)
val comment_decoded = decode(comment)
val cancel_decoded = decode(cancel)
val latex_decoded = decode(latex)
+ val marker_decoded = decode(marker)
val open_decoded = decode(open)
val close_decoded = decode(close)
@@ -579,23 +579,17 @@
else str
- /* marker */
-
- val marker: Symbol = "\\<marker>"
- def marker_decoded: Symbol = symbols.marker_decoded
-
- lazy val is_marker: Set[Symbol] = Set(marker, marker_decoded)
-
-
/* formal comments */
val comment: Symbol = "\\<comment>"
val cancel: Symbol = "\\<^cancel>"
val latex: Symbol = "\\<^latex>"
+ val marker: Symbol = "\\<^marker>"
def comment_decoded: Symbol = symbols.comment_decoded
def cancel_decoded: Symbol = symbols.cancel_decoded
def latex_decoded: Symbol = symbols.latex_decoded
+ def marker_decoded: Symbol = symbols.marker_decoded
/* cartouches */
--- a/src/Pure/Isar/outer_syntax.ML Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Sun Mar 10 21:12:29 2019 +0100
@@ -22,10 +22,10 @@
val local_theory_to_proof: command_keyword -> string ->
(local_theory -> Proof.state) parser -> unit
val bootstrap: bool Config.T
- val parse_tokens: theory -> Token.T list -> Toplevel.transition list
- val parse: theory -> Position.T -> string -> Toplevel.transition list
val parse_spans: Token.T list -> Command_Span.span list
val make_span: Token.T list -> Command_Span.span
+ val parse_span: theory -> (unit -> theory) -> Token.T list -> Toplevel.transition
+ val parse_text: theory -> (unit -> theory) -> Position.T -> string -> Toplevel.transition list
val command_reports: theory -> Token.T -> Position.report_text list
val check_command: Proof.context -> command_keyword -> string
end;
@@ -172,60 +172,6 @@
(** toplevel parsing **)
-(* parse commands *)
-
-val bootstrap = Config.declare_bool ("Outer_Syntax.bootstrap", \<^here>) (K true);
-
-local
-
-val before_command =
- Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false));
-
-fun parse_command thy =
- Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) =>
- let
- val keywords = Thy_Header.get_keywords thy;
- val tr0 =
- Toplevel.empty
- |> Toplevel.name name
- |> Toplevel.position pos
- |> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open
- |> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close;
- val command_marker =
- Parse.command |-- Document_Source.annotation >> (fn markers => Toplevel.markers markers tr0);
- in
- (case lookup_commands thy name of
- SOME (Command {command_parser = Parser parse, ...}) =>
- Parse.!!! (command_marker -- parse) >> (op |>)
- | SOME (Command {command_parser = Restricted_Parser parse, ...}) =>
- before_command :|-- (fn restricted =>
- Parse.!!! (command_marker -- parse restricted)) >> (op |>)
- | NONE =>
- Scan.fail_with (fn _ => fn _ =>
- let
- val msg =
- if Config.get_global thy bootstrap
- then "missing theory context for command "
- else "undefined command ";
- in msg ^ quote (Markup.markup Markup.keyword1 name) end))
- end);
-
-in
-
-fun parse_tokens thy =
- filter Token.is_proper
- #> Source.of_list
- #> Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy) xs))
- #> Source.exhaust;
-
-fun parse thy pos text =
- Symbol_Pos.explode (text, pos)
- |> Token.tokenize (Thy_Header.get_keywords thy) {strict = false}
- |> parse_tokens thy;
-
-end;
-
-
(* parse spans *)
local
@@ -267,6 +213,75 @@
| _ => Command_Span.Span (Command_Span.Malformed_Span, toks));
+(* parse commands *)
+
+val bootstrap = Config.declare_bool ("Outer_Syntax.bootstrap", \<^here>) (K true);
+
+local
+
+val before_command =
+ Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false));
+
+fun parse_command thy markers =
+ Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) =>
+ let
+ val keywords = Thy_Header.get_keywords thy;
+ val tr0 =
+ Toplevel.empty
+ |> Toplevel.name name
+ |> Toplevel.position pos
+ |> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open
+ |> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close;
+ val command_markers =
+ Parse.command |-- Document_Source.tags >>
+ (fn tags => Toplevel.markers (map Document_Marker.legacy_tag tags @ markers) tr0);
+ in
+ (case lookup_commands thy name of
+ SOME (Command {command_parser = Parser parse, ...}) =>
+ Parse.!!! (command_markers -- parse) >> (op |>)
+ | SOME (Command {command_parser = Restricted_Parser parse, ...}) =>
+ before_command :|-- (fn restricted =>
+ Parse.!!! (command_markers -- parse restricted)) >> (op |>)
+ | NONE =>
+ Scan.fail_with (fn _ => fn _ =>
+ let
+ val msg =
+ if Config.get_global thy bootstrap
+ then "missing theory context for command "
+ else "undefined command ";
+ in msg ^ quote (Markup.markup Markup.keyword1 name) end))
+ end);
+
+in
+
+fun parse_span thy init span =
+ let
+ val range = Token.range_of span;
+ val core_range = Token.core_range_of span;
+
+ val markers = map Token.input_of (filter Token.is_document_marker span);
+ fun parse () =
+ filter Token.is_proper span
+ |> Source.of_list
+ |> Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy markers) xs))
+ |> Source.exhaust;
+ in
+ (case parse () of
+ [tr] => Toplevel.modify_init init tr
+ | [] => Toplevel.ignored (#1 range)
+ | _ => Toplevel.malformed (#1 core_range) "Exactly one command expected")
+ handle ERROR msg => Toplevel.malformed (#1 core_range) msg
+ end;
+
+fun parse_text thy init pos text =
+ Symbol_Pos.explode (text, pos)
+ |> Token.tokenize (Thy_Header.get_keywords thy) {strict = false}
+ |> parse_spans
+ |> map (Command_Span.content #> parse_span thy init);
+
+end;
+
+
(* check commands *)
fun command_reports thy tok =
--- a/src/Pure/Isar/parse.ML Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Isar/parse.ML Sun Mar 10 21:12:29 2019 +0100
@@ -96,6 +96,7 @@
val for_fixes: (binding * string option * mixfix) list parser
val ML_source: Input.source parser
val document_source: Input.source parser
+ val document_marker: Input.source parser
val const: string parser
val term: string parser
val prop: string parser
@@ -390,6 +391,10 @@
val ML_source = input (group (fn () => "ML source") text);
val document_source = input (group (fn () => "document source") text);
+val document_marker =
+ group (fn () => "document marker")
+ (RESET_VALUE (Scan.one Token.is_document_marker >> Token.input_of));
+
(* terms *)
--- a/src/Pure/Isar/parse.scala Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Isar/parse.scala Sun Mar 10 21:12:29 2019 +0100
@@ -83,10 +83,9 @@
def tag: Parser[String] = $$$("%") ~> tag_name
def tags: Parser[List[String]] = rep(tag)
- def marker: Parser[String] =
- ($$$(Symbol.marker) | $$$(Symbol.marker_decoded)) ~! embedded ^^ { case _ ~ x => x }
+ def marker: Parser[String] = token("marker", _.is_marker) ^^ (_.content)
- def annotation: Parser[Unit] = rep(marker | tag) ^^ { case _ => () }
+ def annotation: Parser[Unit] = rep(tag | marker) ^^ { case _ => () }
/* wrappers */
--- a/src/Pure/Isar/token.ML Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Isar/token.ML Sun Mar 10 21:12:29 2019 +0100
@@ -30,7 +30,6 @@
Declaration of declaration |
Files of file Exn.result list
val pos_of: T -> Position.T
- val range_of: T list -> Position.range
val adjust_offsets: (int -> int option) -> T -> T
val eof: T
val is_eof: T -> bool
@@ -46,6 +45,7 @@
val is_comment: T -> bool
val is_informal_comment: T -> bool
val is_formal_comment: T -> bool
+ val is_document_marker: T -> bool
val is_ignored: T -> bool
val is_begin_ignore: T -> bool
val is_end_ignore: T -> bool
@@ -53,6 +53,8 @@
val is_space: T -> bool
val is_blank: T -> bool
val is_newline: T -> bool
+ val range_of: T list -> Position.range
+ val core_range_of: T list -> Position.range
val content_of: T -> string
val source_of: T -> string
val input_of: T -> Input.source
@@ -190,11 +192,6 @@
fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos;
-fun range_of (toks as tok :: _) =
- let val pos' = end_pos_of (List.last toks)
- in Position.range (pos_of tok, pos') end
- | range_of [] = Position.no_range;
-
fun adjust_offsets adjust (Token ((x, range), y, z)) =
Token ((x, apply2 (Position.adjust_offsets adjust) range), y, z);
@@ -245,6 +242,9 @@
fun is_formal_comment (Token (_, (Comment (SOME _), _), _)) = true
| is_formal_comment _ = false;
+fun is_document_marker (Token (_, (Comment (SOME Comment.Marker), _), _)) = true
+ | is_document_marker _ = false;
+
fun is_begin_ignore (Token (_, (Comment NONE, "<"), _)) = true
| is_begin_ignore _ = false;
@@ -267,6 +267,17 @@
| is_newline _ = false;
+(* range of tokens *)
+
+fun range_of (toks as tok :: _) =
+ let val pos' = end_pos_of (List.last toks)
+ in Position.range (pos_of tok, pos') end
+ | range_of [] = Position.no_range;
+
+val core_range_of =
+ drop_prefix is_ignored #> drop_suffix is_ignored #> range_of;
+
+
(* token content *)
fun content_of (Token (_, (_, x), _)) = x;
@@ -636,7 +647,7 @@
scan_verbatim >> token_range Verbatim ||
scan_cartouche >> token_range Cartouche ||
scan_comment >> token_range (Comment NONE) ||
- Comment.scan >> (fn (k, ss) => token (Comment (SOME k)) ss) ||
+ Comment.scan_outer >> (fn (k, ss) => token (Comment (SOME k)) ss) ||
scan_space >> token Space ||
(Scan.max token_leq
(Scan.max token_leq
--- a/src/Pure/Isar/token.scala Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Isar/token.scala Sun Mar 10 21:12:29 2019 +0100
@@ -304,6 +304,9 @@
def is_space: Boolean = kind == Token.Kind.SPACE
def is_informal_comment: Boolean = kind == Token.Kind.INFORMAL_COMMENT
def is_formal_comment: Boolean = kind == Token.Kind.FORMAL_COMMENT
+ def is_marker: Boolean =
+ kind == Token.Kind.FORMAL_COMMENT &&
+ (source.startsWith(Symbol.marker) || source.startsWith(Symbol.marker_decoded))
def is_comment: Boolean = is_informal_comment || is_formal_comment
def is_ignored: Boolean = is_space || is_informal_comment
def is_proper: Boolean = !is_space && !is_comment
--- a/src/Pure/ML/ml_lex.ML Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/ML/ml_lex.ML Sun Mar 10 21:12:29 2019 +0100
@@ -312,7 +312,7 @@
val scan_sml_antiq = scan_sml >> Antiquote.Text;
val scan_ml_antiq =
- Comment.scan >> (fn (kind, ss) => Antiquote.Text (token (Comment (SOME kind)) ss)) ||
+ Comment.scan_inner >> (fn (kind, ss) => Antiquote.Text (token (Comment (SOME kind)) ss)) ||
Antiquote.scan_control >> Antiquote.Control ||
Antiquote.scan_antiq >> Antiquote.Antiq ||
scan_rat_antiq >> Antiquote.Antiq ||
--- a/src/Pure/PIDE/command.ML Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/PIDE/command.ML Sun Mar 10 21:12:29 2019 +0100
@@ -155,12 +155,7 @@
Position.here_list verbatim);
in
if exists #1 token_reports then Toplevel.malformed pos "Malformed command syntax"
- else
- (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs_info span) of
- [tr] => Toplevel.modify_init init tr
- | [] => Toplevel.ignored (#1 (Token.range_of span))
- | _ => Toplevel.malformed (#1 core_range) "Exactly one command expected")
- handle ERROR msg => Toplevel.malformed (#1 core_range) msg
+ else Outer_Syntax.parse_span thy init (resolve_files keywords master_dir blobs_info span)
end;
end;
--- a/src/Pure/PIDE/command.scala Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/PIDE/command.scala Sun Mar 10 21:12:29 2019 +0100
@@ -475,7 +475,6 @@
toks match {
case (t1, i1) :: (t2, i2) :: rest =>
if (t1.is_keyword && t1.source == "%" && t2.is_name) clean(rest)
- else if (t1.is_keyword && Symbol.is_marker(t1.source) && t2.is_embedded) clean(rest)
else (t1, i1) :: clean((t2, i2) :: rest)
case _ => toks
}
--- a/src/Pure/Pure.thy Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Pure.thy Sun Mar 10 21:12:29 2019 +0100
@@ -7,7 +7,7 @@
theory Pure
keywords
"!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
- "\<marker>" "\<subseteq>" "]" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output"
+ "\<subseteq>" "]" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output"
"overloaded" "pervasive" "premises" "structure" "unchecked"
and "private" "qualified" :: before_command
and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites"
--- a/src/Pure/Syntax/lexicon.ML Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Syntax/lexicon.ML Sun Mar 10 21:12:29 2019 +0100
@@ -301,7 +301,7 @@
val scan =
Symbol_Pos.scan_cartouche err_prefix >> token Cartouche ||
- Comment.scan >> (fn (kind, ss) => token (Comment kind) ss) ||
+ Comment.scan_inner >> (fn (kind, ss) => token (Comment kind) ss) ||
Scan.max token_leq scan_lit scan_val ||
scan_string >> token String ||
scan_str >> token Str ||
--- a/src/Pure/Thy/document_marker.ML Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Thy/document_marker.ML Sun Mar 10 21:12:29 2019 +0100
@@ -10,6 +10,7 @@
val setup: binding -> 'a context_parser -> ('a -> marker) -> theory -> theory
val setup0: binding -> 'a parser -> ('a -> marker) -> theory -> theory
val evaluate: Input.source -> marker
+ val legacy_tag: string -> Input.source
end;
structure Document_Marker: DOCUMENT_MARKER =
@@ -47,14 +48,14 @@
fun evaluate input ctxt =
let
- val pos = Input.pos_of input;
- val _ = Context_Position.report ctxt pos Markup.language_document_marker;
-
- val syms = Input.source_explode input;
+ val body =
+ Input.source_explode input
+ |> drop_prefix (fn (s, _) => s = Symbol.marker)
+ |> Symbol_Pos.cartouche_content;
val markers =
- (case Token.read_body (Thy_Header.get_keywords' ctxt) (Parse.list parse_marker) syms of
+ (case Token.read_body (Thy_Header.get_keywords' ctxt) (Parse.list parse_marker) body of
SOME res => res
- | NONE => error ("Bad input" ^ Position.here pos));
+ | NONE => error ("Bad input" ^ Position.here (Input.pos_of input)));
in fold (fn src => #2 (check ctxt (Token.name_of_src src)) src) markers ctxt end;
@@ -77,4 +78,7 @@
val _ = Context_Position.report ctxt pos Markup.words;
in meta_data Markup.meta_description arg ctxt end));
+fun legacy_tag name =
+ Input.string (cartouche ("tag " ^ Symbol_Pos.quote_string_qq name));
+
end;
--- a/src/Pure/Thy/document_source.ML Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Thy/document_source.ML Sun Mar 10 21:12:29 2019 +0100
@@ -17,7 +17,7 @@
val get_tags: Proof.context -> string list
val update_tags: string -> Proof.context -> Proof.context
val tags: string list parser
- val annotation: Input.source list parser
+ val annotation: unit parser
end;
structure Document_Source: DOCUMENT_SOURCE =
@@ -62,13 +62,8 @@
(* semantic markers (operation on presentation context) *)
-val marker =
- (improper -- Parse.$$$ "\<marker>" -- improper) |--
- Parse.!!! (Parse.group (fn () => "document marker") (Parse.input Parse.embedded) --| blank_end);
+val marker = improper |-- Parse.document_marker --| blank_end;
-val tag_marker = (*emulation of old-style tags*)
- tag >> (fn name => Input.string ("tag " ^ Symbol_Pos.quote_string_qq name));
-
-val annotation = Scan.repeat (marker || tag_marker);
+val annotation = Scan.repeat (tag >> K () || marker >> K ()) >> K ();
end;
--- a/src/Pure/Thy/thy_header.ML Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Thy/thy_header.ML Sun Mar 10 21:12:29 2019 +0100
@@ -175,10 +175,10 @@
Parse.command_name textN ||
Parse.command_name txtN ||
Parse.command_name text_rawN) --
- Document_Source.annotation -- Parse.!!! Parse.document_source;
+ (Document_Source.annotation |-- Parse.!!! Parse.document_source);
val parse_header =
- (Scan.repeat heading -- Parse.command_name theoryN -- Document_Source.annotation)
+ (Scan.repeat heading -- Parse.command_name theoryN --| Document_Source.annotation)
|-- Parse.!!! args;
fun read_tokens pos toks =
--- a/src/Pure/Thy/thy_info.ML Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Thy/thy_info.ML Sun Mar 10 21:12:29 2019 +0100
@@ -451,9 +451,7 @@
fun script_thy pos txt thy =
let
- val trs =
- Outer_Syntax.parse thy pos txt
- |> map (Toplevel.modify_init (K thy));
+ val trs = Outer_Syntax.parse_text thy (K thy) pos txt;
val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ());
in Toplevel.end_theory end_pos end_state end;
--- a/src/Pure/Thy/thy_output.ML Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Thy/thy_output.ML Sun Mar 10 21:12:29 2019 +0100
@@ -61,8 +61,8 @@
Symbol_Pos.cartouche_content syms
|> output_symbols
|> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
- | Comment.Latex =>
- [Latex.symbols (Symbol_Pos.cartouche_content syms)])
+ | Comment.Latex => [Latex.symbols (Symbol_Pos.cartouche_content syms)]
+ | Comment.Marker => [])
and output_comment_document ctxt (comment, syms) =
(case comment of
SOME kind => output_comment ctxt (kind, syms)
@@ -139,6 +139,7 @@
in
(case Token.kind_of tok of
Token.Comment NONE => []
+ | Token.Comment (SOME Comment.Marker) => []
| Token.Command => output false "\\isacommand{" "}"
| Token.Keyword =>
if Symbol.is_ascii_identifier (Token.content_of tok)
--- a/src/Pure/Tools/rail.ML Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Tools/rail.ML Sun Mar 10 21:12:29 2019 +0100
@@ -118,7 +118,7 @@
val scan_token =
scan_space >> token Space ||
- Comment.scan >> (fn (kind, ss) => token (Comment kind) ss)||
+ Comment.scan_inner >> (fn (kind, ss) => token (Comment kind) ss) ||
Antiquote.scan_antiq >> antiq_token ||
scan_keyword >> (token Keyword o single) ||
Lexicon.scan_id >> token Ident ||