equal
deleted
inserted
replaced
36 val adjust_offsets: (int -> int option) -> T -> T |
36 val adjust_offsets: (int -> int option) -> T -> T |
37 val of_properties: Properties.T -> T |
37 val of_properties: Properties.T -> T |
38 val properties_of: T -> Properties.T |
38 val properties_of: T -> Properties.T |
39 val offset_properties_of: T -> Properties.T |
39 val offset_properties_of: T -> Properties.T |
40 val def_properties_of: T -> Properties.T |
40 val def_properties_of: T -> Properties.T |
|
41 val entity_markup: string -> string * T -> Markup.T |
41 val entity_properties_of: bool -> serial -> T -> Properties.T |
42 val entity_properties_of: bool -> serial -> T -> Properties.T |
42 val default_properties: T -> Properties.T -> Properties.T |
43 val default_properties: T -> Properties.T -> Properties.T |
43 val markup: T -> Markup.T -> Markup.T |
44 val markup: T -> Markup.T -> Markup.T |
44 val is_reported: T -> bool |
45 val is_reported: T -> bool |
45 val is_reported_range: T -> bool |
46 val is_reported_range: T -> bool |
201 fun offset_properties_of (Pos ((_, j, k), _)) = |
202 fun offset_properties_of (Pos ((_, j, k), _)) = |
202 value Markup.offsetN j @ value Markup.end_offsetN k; |
203 value Markup.offsetN j @ value Markup.end_offsetN k; |
203 |
204 |
204 val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y)); |
205 val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y)); |
205 |
206 |
|
207 fun entity_markup kind (name, pos) = |
|
208 Markup.entity kind name |> Markup.properties (def_properties_of pos); |
|
209 |
206 fun entity_properties_of def serial pos = |
210 fun entity_properties_of def serial pos = |
207 if def then (Markup.defN, Value.print_int serial) :: properties_of pos |
211 if def then (Markup.defN, Value.print_int serial) :: properties_of pos |
208 else (Markup.refN, Value.print_int serial) :: def_properties_of pos; |
212 else (Markup.refN, Value.print_int serial) :: def_properties_of pos; |
209 |
213 |
210 fun default_properties default props = |
214 fun default_properties default props = |