--- a/src/Pure/General/markup.ML Sun Jul 08 19:52:05 2007 +0200
+++ b/src/Pure/General/markup.ML Sun Jul 08 19:52:08 2007 +0200
@@ -8,10 +8,11 @@
signature MARKUP =
sig
type property = string * string
+ type T = string * property list
val nameN: string
+ val kindN: string
val pos_lineN: string
val pos_nameN: string
- type T = string * property list
val none: T
val indentN: string
val blockN: string val block: int -> T
@@ -35,23 +36,20 @@
structure Markup: MARKUP =
struct
-(* properties *)
+(* basic markup *)
type property = string * string;
-
-val nameN = "name";
-val pos_lineN = "pos_line";
-val pos_nameN = "pos_name";
-
-
-(* markup *)
-
type T = string * property list;
val none = ("", []);
+val nameN = "name";
+val kindN = "kind";
+val pos_lineN = "pos_line";
+val pos_nameN = "pos_name";
+
fun markup kind = (kind, (kind, []): T);
-fun markup_name kind = (kind, fn name => (kind, [(nameN, name)]): T);
+fun markup_string kind prop = (kind, fn s => (kind, [(prop, s)]): T);
fun markup_int kind prop = (kind, fn i => (kind, [(prop, string_of_int i)]): T);
@@ -68,10 +66,10 @@
(* logical entities *)
-val (classN, class) = markup_name "class";
-val (tyconN, tycon) = markup_name "tycon";
-val (constN, const) = markup_name "const";
-val (axiomN, axiom) = markup_name "axiom";
+val (classN, class) = markup_string "class" nameN;
+val (tyconN, tycon) = markup_string "tycon" nameN;
+val (constN, const) = markup_string "const" nameN;
+val (axiomN, axiom) = markup_string "axiom" nameN;
(* inner syntax *)
@@ -83,8 +81,8 @@
(* outer syntax *)
-val (keywordN, keyword) = markup_name "keyword";
-val (commandN, command) = markup_name "command";
+val (keywordN, keyword) = markup_string "keyword" nameN;
+val (commandN, command) = markup_string "command" nameN;
(* toplevel *)