author | wenzelm |
Mon, 28 Nov 2011 22:05:32 +0100 | |
changeset 45666 | d83797ef0d2d |
parent 45448 | 018f8959c7a6 |
child 49674 | dbadb4d03cbc |
permissions | -rw-r--r-- |
42264 | 1 |
(* Title: Pure/Syntax/term_position.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Encoded position within term syntax trees. |
|
5 |
*) |
|
6 |
||
7 |
signature TERM_POSITION = |
|
8 |
sig |
|
9 |
val pretty: Position.T -> Pretty.T |
|
10 |
val encode: Position.T -> string |
|
11 |
val decode: string -> Position.T option |
|
45445
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
42264
diff
changeset
|
12 |
val decode_position: term -> (Position.T * typ) option |
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
42264
diff
changeset
|
13 |
val decode_positionT: typ -> Position.T option |
42264 | 14 |
val is_position: term -> bool |
45448
018f8959c7a6
more efficient prepare_sorts -- bypass encoded positions;
wenzelm
parents:
45445
diff
changeset
|
15 |
val is_positionT: typ -> bool |
42264 | 16 |
val strip_positions: term -> term |
17 |
end; |
|
18 |
||
19 |
structure Term_Position: TERM_POSITION = |
|
20 |
struct |
|
21 |
||
22 |
(* markup *) |
|
23 |
||
24 |
val position_dummy = "<position>"; |
|
25 |
val position_text = XML.Text position_dummy; |
|
26 |
||
27 |
fun pretty pos = |
|
45666 | 28 |
Pretty.markup (Position.markup pos Isabelle_Markup.position) [Pretty.str position_dummy]; |
42264 | 29 |
|
30 |
fun encode pos = |
|
45666 | 31 |
YXML.string_of (XML.Elem (Position.markup pos Isabelle_Markup.position, [position_text])); |
42264 | 32 |
|
33 |
fun decode str = |
|
34 |
(case YXML.parse_body str handle Fail msg => error msg of |
|
35 |
[XML.Elem ((name, props), [arg])] => |
|
45666 | 36 |
if name = Isabelle_Markup.positionN andalso arg = position_text |
42264 | 37 |
then SOME (Position.of_properties props) |
38 |
else NONE |
|
39 |
| _ => NONE); |
|
40 |
||
41 |
||
42 |
(* positions within parse trees *) |
|
43 |
||
45445
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
42264
diff
changeset
|
44 |
fun decode_position (Free (x, _)) = |
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
42264
diff
changeset
|
45 |
(case decode x of |
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
42264
diff
changeset
|
46 |
SOME pos => SOME (pos, TFree (x, dummyS)) |
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
42264
diff
changeset
|
47 |
| NONE => NONE) |
42264 | 48 |
| decode_position _ = NONE; |
49 |
||
45445
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
42264
diff
changeset
|
50 |
fun decode_positionT (TFree (x, _)) = decode x |
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
42264
diff
changeset
|
51 |
| decode_positionT _ = NONE; |
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
42264
diff
changeset
|
52 |
|
42264 | 53 |
val is_position = is_some o decode_position; |
45448
018f8959c7a6
more efficient prepare_sorts -- bypass encoded positions;
wenzelm
parents:
45445
diff
changeset
|
54 |
val is_positionT = is_some o decode_positionT; |
42264 | 55 |
|
56 |
fun strip_positions ((t as Const (c, _)) $ u $ v) = |
|
57 |
if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v |
|
58 |
then strip_positions u |
|
59 |
else t $ strip_positions u $ strip_positions v |
|
60 |
| strip_positions (t $ u) = strip_positions t $ strip_positions u |
|
61 |
| strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t) |
|
62 |
| strip_positions t = t; |
|
63 |
||
64 |
end; |