src/Pure/Isar/method.ML

--- a/src/Pure/Isar/method.ML	Tue Oct 16 17:47:23 2012 +0200
+++ b/src/Pure/Isar/method.ML	Tue Oct 16 20:23:00 2012 +0200
@@ -73,7 +73,10 @@
   type modifier = (Proof.context -> Proof.context) * attribute
   val section: modifier parser list -> thm list context_parser
   val sections: modifier parser list -> thm list list context_parser
-  val parse: text parser
+  type text_position = text * Position.T
+  val parse: text_position parser
+  val text: text_position option -> text option
+  val position: text_position option -> Position.T
 end;
 
 structure Method: METHOD =
@@ -411,7 +414,23 @@
 and meth1 x = (Parse.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
 and meth0 x = (Parse.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
 
-in val parse = meth3 end;
+in
+
+val parse =
+  Scan.trace meth3 >> (fn (m, toks) => (m, Position.set_range (Token.position_range_of toks)));
+
+end;
+
+
+(* text position *)
+
+type text_position = text * Position.T;
+
+fun text NONE = NONE
+  | text (SOME (txt, _)) = SOME txt;
+
+fun position NONE = Position.none
+  | position (SOME (_, pos)) = pos;
 
 
 (* theory setup *)