--- a/src/Pure/Isar/outer_syntax.ML Tue Jan 23 20:43:18 2018 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Wed Jan 24 11:56:38 2018 +0100
@@ -285,7 +285,7 @@
if Keyword.is_command keywords name then
let
val markup =
- Token.explode keywords Position.none name
+ Token.explode0 keywords name
|> maps (command_reports thy)
|> map (#2 o #1);
val _ = Context_Position.reports ctxt (map (pair pos) markup);
--- a/src/Pure/Isar/token.ML Tue Jan 23 20:43:18 2018 +0100
+++ b/src/Pure/Isar/token.ML Wed Jan 24 11:56:38 2018 +0100
@@ -92,7 +92,9 @@
Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
(Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
val read_cartouche: Symbol_Pos.T list -> T
+ val tokenize: Keyword.keywords -> Symbol_Pos.T list -> T list
val explode: Keyword.keywords -> Position.T -> string -> T list
+ val explode0: Keyword.keywords -> string -> T list
val print_name: Keyword.keywords -> string -> string
val make: (int * int) * string -> Position.T -> T * Position.T
val make_string: string * Position.T -> T
@@ -669,11 +671,13 @@
(* explode *)
-fun explode keywords pos =
- Symbol.explode #>
- Source.of_list #>
- source keywords pos #>
- Source.exhaust;
+fun tokenize keywords syms =
+ Source.of_list syms |> source' false keywords |> Source.exhaust;
+
+fun explode keywords pos text =
+ Symbol_Pos.explode (text, pos) |> tokenize keywords;
+
+fun explode0 keywords = explode keywords Position.none;
(* print name in parsable form *)
--- a/src/Pure/Thy/document_antiquotations.ML Tue Jan 23 20:43:18 2018 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML Wed Jan 24 11:56:38 2018 +0100
@@ -184,7 +184,7 @@
|> Context_Position.reports_text ctxt;
in
prepare_text ctxt text
- |> Token.explode keywords Position.none
+ |> Token.explode0 keywords
|> maps (Thy_Output.output_token ctxt)
|> Thy_Output.isabelle ctxt
end);