# HG changeset patch # User wenzelm # Date 1516791398 -3600 # Node ID 90d760fa8f34480b334a101762f0f689c98327f0 # Parent b8e093f7a802e463efe8228975faadacd2596284 clarified operations; diff -r b8e093f7a802 -r 90d760fa8f34 src/Pure/Isar/outer_syntax.ML --- 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); diff -r b8e093f7a802 -r 90d760fa8f34 src/Pure/Isar/token.ML --- 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 *) diff -r b8e093f7a802 -r 90d760fa8f34 src/Pure/Thy/document_antiquotations.ML --- 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);