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.;
wenzelm@42264
     1
(*  Title:      Pure/Syntax/term_position.ML
wenzelm@42264
     2
    Author:     Makarius
wenzelm@42264
     3
wenzelm@42264
     4
Encoded position within term syntax trees.
wenzelm@42264
     5
*)
wenzelm@42264
     6
wenzelm@42264
     7
signature TERM_POSITION =
wenzelm@42264
     8
sig
wenzelm@42264
     9
  val pretty: Position.T -> Pretty.T
wenzelm@42264
    10
  val encode: Position.T -> string
wenzelm@42264
    11
  val decode: string -> Position.T option
wenzelm@45445
    12
  val decode_position: term -> (Position.T * typ) option
wenzelm@45445
    13
  val decode_positionT: typ -> Position.T option
wenzelm@49685
    14
  val decode_positionS: sort -> Position.T list * sort
wenzelm@42264
    15
  val is_position: term -> bool
wenzelm@45448
    16
  val is_positionT: typ -> bool
wenzelm@42264
    17
  val strip_positions: term -> term
wenzelm@42264
    18
end;
wenzelm@42264
    19
wenzelm@42264
    20
structure Term_Position: TERM_POSITION =
wenzelm@42264
    21
struct
wenzelm@42264
    22
wenzelm@42264
    23
(* markup *)
wenzelm@42264
    24
wenzelm@42264
    25
val position_dummy = "<position>";
wenzelm@42264
    26
val position_text = XML.Text position_dummy;
wenzelm@42264
    27
wenzelm@42264
    28
fun pretty pos =
wenzelm@50201
    29
  Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy];
wenzelm@42264
    30
wenzelm@42264
    31
fun encode pos =
wenzelm@50201
    32
  YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text]));
wenzelm@42264
    33
wenzelm@42264
    34
fun decode str =
wenzelm@42264
    35
  (case YXML.parse_body str handle Fail msg => error msg of
wenzelm@42264
    36
    [XML.Elem ((name, props), [arg])] =>
wenzelm@50201
    37
      if name = Markup.positionN andalso arg = position_text
wenzelm@42264
    38
      then SOME (Position.of_properties props)
wenzelm@42264
    39
      else NONE
wenzelm@42264
    40
  | _ => NONE);
wenzelm@42264
    41
wenzelm@42264
    42
wenzelm@42264
    43
(* positions within parse trees *)
wenzelm@42264
    44
wenzelm@45445
    45
fun decode_position (Free (x, _)) =
wenzelm@45445
    46
      (case decode x of
wenzelm@45445
    47
        SOME pos => SOME (pos, TFree (x, dummyS))
wenzelm@45445
    48
      | NONE => NONE)
wenzelm@42264
    49
  | decode_position _ = NONE;
wenzelm@42264
    50
wenzelm@45445
    51
fun decode_positionT (TFree (x, _)) = decode x
wenzelm@45445
    52
  | decode_positionT _ = NONE;
wenzelm@45445
    53
wenzelm@49685
    54
fun decode_positionS cs =
wenzelm@49685
    55
  let val (ps, sort) = List.partition (is_some o decode) cs
wenzelm@49685
    56
  in (map (the o decode) ps, sort) end;
wenzelm@49674
    57
wenzelm@42264
    58
val is_position = is_some o decode_position;
wenzelm@45448
    59
val is_positionT = is_some o decode_positionT;
wenzelm@42264
    60
wenzelm@42264
    61
fun strip_positions ((t as Const (c, _)) $ u $ v) =
wenzelm@49674
    62
      if (c = "_constrain" orelse c = "_constrainAbs" orelse c = "_ofsort") andalso is_position v
wenzelm@42264
    63
      then strip_positions u
wenzelm@42264
    64
      else t $ strip_positions u $ strip_positions v
wenzelm@42264
    65
  | strip_positions (t $ u) = strip_positions t $ strip_positions u
wenzelm@42264
    66
  | strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t)
wenzelm@42264
    67
  | strip_positions t = t;
wenzelm@42264
    68
wenzelm@42264
    69
end;