--- a/src/Pure/Thy/document_marker.ML Wed Oct 20 11:34:28 2021 +0200
+++ b/src/Pure/Thy/document_marker.ML Wed Oct 20 16:36:49 2021 +0200
@@ -59,11 +59,11 @@
val _ = Context_Position.reports ctxt (map (pair pos) (Comment.kind_markups Comment.Marker));
+ val keywords = Keyword.no_command_keywords (Thy_Header.get_keywords' ctxt);
val body = Symbol_Pos.cartouche_content syms;
val markers =
- (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));
+ Input.source true (Symbol_Pos.implode body) (Symbol_Pos.range body)
+ |> Token.read_embedded ctxt keywords (Parse.list parse_marker);
in
ctxt
|> Config.put config_command_name cmd_name