# HG changeset patch
# User wenzelm
# Date 1183760230 -7200
# Node ID 939b58b527eecc50254890e85c0c3ed8f29abf59
# Parent  8ce09f6926532ec74a29b71b05577d9bc45c1d66
Common markup elements.

diff -r 8ce09f692653 -r 939b58b527ee src/Pure/General/markup.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/markup.ML	Sat Jul 07 00:17:10 2007 +0200
@@ -0,0 +1,103 @@
+(*  Title:      Pure/General/markup.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Common markup elements.
+*)
+
+signature MARKUP =
+sig
+  type property = string * string
+  type T = string * property list
+  val none: T
+  val property: string * string -> T -> T
+  val nameN: string
+  val add_name: string -> T -> T
+  val posN: string
+  val add_pos: Position.T -> T -> T
+  val classN: string
+  val class: string -> T
+  val tyconN: string
+  val tycon: string -> T
+  val constN: string
+  val const: string -> T
+  val axiomN: string
+  val axiom: string -> T
+  val sortN: string
+  val sort: T
+  val typN: string
+  val typ: T
+  val termN: string
+  val term: T
+  val propN: string
+  val prop: T
+  val thmN: string
+  val thm: T
+  val keywordN: string
+  val keyword: string -> T
+  val commandN: string
+  val command: string -> T
+end;
+
+structure Markup: MARKUP =
+struct
+
+type property = string * string;
+type T = string * property list;
+
+val none = ("", []);
+
+
+(* properties *)
+
+fun property x (name, xs) : T = (name, x :: xs);
+
+val nameN = "name";
+fun add_name x = property (nameN, x);
+
+val posN = "pos";
+fun add_pos x = property (posN, Position.str_of x);
+
+
+(* logical entities *)
+
+val classN = "class";
+fun class name = (classN, [(nameN, name)]);
+
+val tyconN = "tycon";
+fun tycon name = (tyconN, [(nameN, name)]);
+
+val constN = "const";
+fun const name = (constN, [(nameN, name)]);
+
+val axiomN = "axiom";
+fun axiom name = (axiomN, [(nameN, name)]);
+
+
+(* inner syntax *)
+
+val sortN = "sort";
+val sort = (sortN, []);
+
+val typN = "typ";
+val typ = (typN, []);
+
+val termN = "term";
+val term = (termN, []);
+
+val propN = "prop";
+val prop = (propN, []);
+
+val thmN = "thm";
+val thm = (thmN, []);
+
+
+(* outer syntax *)
+
+val keywordN = "keyword";
+fun keyword name = (keywordN, [(nameN, name)]);
+
+val commandN = "command";
+fun command name = (commandN, [(nameN, name)]);
+
+end;