src/Pure/Syntax/term_position.ML
author wenzelm
Wed Dec 12 23:36:07 2012 +0100 (2012-12-12 ago)
changeset 50499 f496b2b7bafb
parent 50201 c26369c9eda6
child 52175 626a757d3c2d
permissions -rw-r--r--
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
     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
    12   val decode_position: term -> (Position.T * typ) option
    13   val decode_positionT: typ -> Position.T option
    14   val decode_positionS: sort -> Position.T list * sort
    15   val is_position: term -> bool
    16   val is_positionT: typ -> bool
    17   val strip_positions: term -> term
    18 end;
    19 
    20 structure Term_Position: TERM_POSITION =
    21 struct
    22 
    23 (* markup *)
    24 
    25 val position_dummy = "<position>";
    26 val position_text = XML.Text position_dummy;
    27 
    28 fun pretty pos =
    29   Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy];
    30 
    31 fun encode pos =
    32   YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text]));
    33 
    34 fun decode str =
    35   (case YXML.parse_body str handle Fail msg => error msg of
    36     [XML.Elem ((name, props), [arg])] =>
    37       if name = Markup.positionN andalso arg = position_text
    38       then SOME (Position.of_properties props)
    39       else NONE
    40   | _ => NONE);
    41 
    42 
    43 (* positions within parse trees *)
    44 
    45 fun decode_position (Free (x, _)) =
    46       (case decode x of
    47         SOME pos => SOME (pos, TFree (x, dummyS))
    48       | NONE => NONE)
    49   | decode_position _ = NONE;
    50 
    51 fun decode_positionT (TFree (x, _)) = decode x
    52   | decode_positionT _ = NONE;
    53 
    54 fun decode_positionS cs =
    55   let val (ps, sort) = List.partition (is_some o decode) cs
    56   in (map (the o decode) ps, sort) end;
    57 
    58 val is_position = is_some o decode_position;
    59 val is_positionT = is_some o decode_positionT;
    60 
    61 fun strip_positions ((t as Const (c, _)) $ u $ v) =
    62       if (c = "_constrain" orelse c = "_constrainAbs" orelse c = "_ofsort") andalso is_position v
    63       then strip_positions u
    64       else t $ strip_positions u $ strip_positions v
    65   | strip_positions (t $ u) = strip_positions t $ strip_positions u
    66   | strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t)
    67   | strip_positions t = t;
    68 
    69 end;