proper position markup;
authorwenzelm
Mon Jul 09 23:12:35 2007 +0200 (2007-07-09)
changeset 236719e8257472c27
parent 23670 681ffad36776
child 23672 3fd7770f6795
proper position markup;
added properties operation;
tuned;
src/Pure/General/markup.ML
     1.1 --- a/src/Pure/General/markup.ML	Mon Jul 09 23:12:31 2007 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Mon Jul 09 23:12:35 2007 +0200
     1.3 @@ -11,9 +11,11 @@
     1.4    type T = string * property list
     1.5    val nameN: string
     1.6    val kindN: string
     1.7 -  val pos_lineN: string
     1.8 -  val pos_nameN: string
     1.9    val none: T
    1.10 +  val properties: (string * string) list -> T -> T
    1.11 +  val lineN: string
    1.12 +  val fileN: string
    1.13 +  val positionN: string val position: T
    1.14    val indentN: string
    1.15    val blockN: string val block: int -> T
    1.16    val breakN: string val break: int -> T
    1.17 @@ -43,14 +45,23 @@
    1.18  
    1.19  val none = ("", []);
    1.20  
    1.21 +fun properties more_props ((elem, props): T) =
    1.22 +  (elem, fold_rev (AList.update (op =)) more_props props);
    1.23 +
    1.24  val nameN = "name";
    1.25  val kindN = "kind";
    1.26 -val pos_lineN = "pos_line";
    1.27 -val pos_nameN = "pos_name";
    1.28 +
    1.29 +fun markup elem = (elem, (elem, []): T);
    1.30 +fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
    1.31 +fun markup_int elem prop = (elem, fn i => (elem, [(prop, string_of_int i)]): T);
    1.32 +
    1.33  
    1.34 -fun markup kind = (kind, (kind, []): T);
    1.35 -fun markup_string kind prop = (kind, fn s => (kind, [(prop, s)]): T);
    1.36 -fun markup_int kind prop = (kind, fn i => (kind, [(prop, string_of_int i)]): T);
    1.37 +(* position *)
    1.38 +
    1.39 +val lineN = "line";
    1.40 +val fileN = "file";
    1.41 +
    1.42 +val (positionN, position) = markup "position";
    1.43  
    1.44  
    1.45  (* pretty printing *)