src/Pure/General/markup.ML
changeset 25816 d2a94e6a7d1e
parent 25808 c7aaa3f6f0ac
child 25844 8943e72bf92a
equal deleted inserted replaced
25815:c7b1e7b7087b 25816:d2a94e6a7d1e
    94 fun markup_elem elem = (elem, (elem, []): T);
    94 fun markup_elem elem = (elem, (elem, []): T);
    95 fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
    95 fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
    96 fun markup_int elem prop = (elem, fn i => (elem, [(prop, Int.toString i)]): T);
    96 fun markup_int elem prop = (elem, fn i => (elem, [(prop, Int.toString i)]): T);
    97 
    97 
    98 val nameN = "name";
    98 val nameN = "name";
    99 val idN = "id";
       
   100 
    99 
   101 
   100 
   102 (* kind *)
   101 (* kind *)
   103 
   102 
   104 val kindN = "kind";
   103 val kindN = "kind";
   109 
   108 
   110 (* position *)
   109 (* position *)
   111 
   110 
   112 val lineN = "line";
   111 val lineN = "line";
   113 val fileN = "file";
   112 val fileN = "file";
       
   113 val idN = "id";
   114 
   114 
   115 val (positionN, position) = markup_elem "position";
   115 val (positionN, position) = markup_elem "position";
   116 
   116 
   117 
   117 
   118 (* pretty printing *)
   118 (* pretty printing *)