equal
deleted
inserted
replaced
19 fun props_of (loc: PolyML.location) = |
19 fun props_of (loc: PolyML.location) = |
20 (case YXML.parse_body (#file loc) of |
20 (case YXML.parse_body (#file loc) of |
21 [] => [] |
21 [] => [] |
22 | [XML.Text file] => |
22 | [XML.Text file] => |
23 if file = "Standard Basis" then [] |
23 if file = "Standard Basis" then [] |
24 else [(Markup.fileN, ml_standard_path file)] |
24 else [(Markup.fileN, ML_System.standard_path file)] |
25 | body => XML.Decode.properties body); |
25 | body => XML.Decode.properties body); |
26 |
26 |
27 fun position_of loc = |
27 fun position_of loc = |
28 Position.make |
28 Position.make |
29 {line = FixedInt.toInt (#startLine loc), |
29 {line = FixedInt.toInt (#startLine loc), |