--- a/src/Pure/General/position.ML Fri Jan 02 11:31:40 2009 +0100
+++ b/src/Pure/General/position.ML Fri Jan 02 15:44:32 2009 +0100
@@ -1,8 +1,7 @@
(* Title: Pure/General/position.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
-Source positions: counting Isabelle symbols -- starting from 1.
+Source positions: counting Isabelle symbols, starting from 1.
*)
signature POSITION =
@@ -19,6 +18,7 @@
val file: string -> T
val line: int -> T
val line_file: int -> string -> T
+ val id: string -> T
val get_id: T -> string option
val put_id: string -> T -> T
val of_properties: Properties.T -> T
@@ -86,6 +86,7 @@
val none = Pos ((0, 0, 0), []);
val start = Pos ((1, 1, 1), []);
+
fun file_name "" = []
| file_name name = [(Markup.fileN, name)];
@@ -95,11 +96,14 @@
fun line i = line_file i "";
-(* markup properties *)
+fun id id = Pos ((0, 0, 1), [(Markup.idN, id)]);
fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
+
+(* markup properties *)
+
fun of_properties props =
let
fun get name =