--- a/src/Pure/Isar/outer_parse.ML Thu Aug 14 19:52:36 2008 +0200
+++ b/src/Pure/Isar/outer_parse.ML Thu Aug 14 19:52:37 2008 +0200
@@ -85,6 +85,8 @@
val fixes: token list -> (string * string option * mixfix) list * token list
val for_fixes: token list -> (string * string option * mixfix) list * token list
val for_simple_fixes: token list -> (string * string option) list * token list
+ val ml_source: token list -> (SymbolPos.text * Position.T) * token list
+ val doc_source: token list -> (SymbolPos.text * Position.T) * token list
val term_group: token list -> string * token list
val prop_group: token list -> string * token list
val term: token list -> string * token list
@@ -152,6 +154,7 @@
val not_eof = RESET_VALUE (Scan.one T.not_eof);
fun position scan = (Scan.ahead not_eof >> T.position_of) -- scan >> Library.swap;
+fun source_position atom = Scan.ahead atom |-- not_eof >> T.source_of';
fun inner_syntax atom = Scan.ahead atom |-- not_eof >> T.source_of;
fun kind k =
@@ -299,6 +302,12 @@
val for_simple_fixes = Scan.optional ($$$ "for" |-- !!! simple_fixes) [];
+(* embedded text *)
+
+val ml_source = source_position (group "ML source" text);
+val doc_source = source_position (group "document source" text);
+
+
(* terms *)
val trm = short_ident || long_ident || sym_ident || term_var || number || string;