src/Pure/General/antiquote.ML
author wenzelm
Tue Mar 24 11:57:41 2009 +0100 (2009-03-24)
changeset 30683 e8ac1f9d9469
parent 30641 72980f8d7ee8
child 39507 839873937ddd
permissions -rw-r--r--
datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
wenzelm@30587
     1
(*  Title:      Pure/General/antiquote.ML
wenzelm@9138
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@9138
     3
wenzelm@30587
     4
Text with antiquotations of inner items (types, terms, theorems etc.).
wenzelm@9138
     5
*)
wenzelm@9138
     6
wenzelm@9138
     7
signature ANTIQUOTE =
wenzelm@9138
     8
sig
wenzelm@30590
     9
  datatype 'a antiquote =
wenzelm@30590
    10
    Text of 'a |
wenzelm@30683
    11
    Antiq of Symbol_Pos.T list * Position.range |
wenzelm@30590
    12
    Open of Position.T |
wenzelm@30590
    13
    Close of Position.T
wenzelm@30635
    14
  val is_text: 'a antiquote -> bool
wenzelm@30641
    15
  val report: ('a -> unit) -> 'a antiquote -> unit
wenzelm@30641
    16
  val check_nesting: 'a antiquote list -> unit
wenzelm@30590
    17
  val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
wenzelm@30590
    18
  val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
wenzelm@30641
    19
  val read: Symbol_Pos.T list * Position.T -> Symbol_Pos.T list antiquote list
wenzelm@9138
    20
end;
wenzelm@9138
    21
wenzelm@9138
    22
structure Antiquote: ANTIQUOTE =
wenzelm@9138
    23
struct
wenzelm@9138
    24
wenzelm@9138
    25
(* datatype antiquote *)
wenzelm@9138
    26
wenzelm@30590
    27
datatype 'a antiquote =
wenzelm@30590
    28
  Text of 'a |
wenzelm@30683
    29
  Antiq of Symbol_Pos.T list * Position.range |
wenzelm@27342
    30
  Open of Position.T |
wenzelm@27342
    31
  Close of Position.T;
wenzelm@9138
    32
wenzelm@30635
    33
fun is_text (Text _) = true
wenzelm@30635
    34
  | is_text _ = false;
wenzelm@27342
    35
wenzelm@27342
    36
wenzelm@30641
    37
(* report *)
wenzelm@30641
    38
wenzelm@30641
    39
val report_antiq = Position.report Markup.antiq;
wenzelm@30641
    40
wenzelm@30641
    41
fun report report_text (Text x) = report_text x
wenzelm@30683
    42
  | report _ (Antiq (_, (pos, _))) = report_antiq pos
wenzelm@30641
    43
  | report _ (Open pos) = report_antiq pos
wenzelm@30641
    44
  | report _ (Close pos) = report_antiq pos;
wenzelm@30641
    45
wenzelm@30641
    46
wenzelm@27342
    47
(* check_nesting *)
wenzelm@27342
    48
wenzelm@27342
    49
fun err_unbalanced pos =
wenzelm@27342
    50
  error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos);
wenzelm@27342
    51
wenzelm@27342
    52
fun check_nesting antiqs =
wenzelm@27342
    53
  let
wenzelm@27342
    54
    fun check [] [] = ()
wenzelm@27342
    55
      | check [] (pos :: _) = err_unbalanced pos
wenzelm@27342
    56
      | check (Open pos :: ants) ps = check ants (pos :: ps)
wenzelm@27342
    57
      | check (Close pos :: _) [] = err_unbalanced pos
wenzelm@27342
    58
      | check (Close _ :: ants) (_ :: ps) = check ants ps
wenzelm@27342
    59
      | check (_ :: ants) ps = check ants ps;
wenzelm@27342
    60
  in check antiqs [] end;
wenzelm@9138
    61
wenzelm@9138
    62
wenzelm@30590
    63
(* scan *)
wenzelm@9138
    64
wenzelm@30573
    65
open Basic_Symbol_Pos;
wenzelm@9138
    66
wenzelm@22114
    67
local
wenzelm@9138
    68
wenzelm@9138
    69
val scan_txt =
wenzelm@27767
    70
  $$$ "@" --| Scan.ahead (~$$$ "{") ||
wenzelm@27767
    71
  Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
wenzelm@27767
    72
    andalso Symbol.is_regular s) >> single;
wenzelm@9138
    73
wenzelm@9138
    74
val scan_ant =
wenzelm@30587
    75
  Symbol_Pos.scan_quoted ||
wenzelm@27767
    76
  Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
wenzelm@9138
    77
wenzelm@9138
    78
val scan_antiq =
wenzelm@30573
    79
  Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
wenzelm@30587
    80
    Symbol_Pos.!!! "missing closing brace of antiquotation"
wenzelm@30573
    81
      (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
wenzelm@30683
    82
  >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
wenzelm@30590
    83
wenzelm@30590
    84
val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
wenzelm@30590
    85
val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>";
wenzelm@9138
    86
wenzelm@9138
    87
in
wenzelm@9138
    88
wenzelm@30590
    89
fun scan x = (scan_antiq >> Antiq || scan_open >> Open || scan_close >> Close) x;
wenzelm@30590
    90
val scan_text = scan || Scan.repeat1 scan_txt >> (Text o flat);
wenzelm@9138
    91
wenzelm@9138
    92
end;
wenzelm@9138
    93
wenzelm@9138
    94
wenzelm@27767
    95
(* read *)
wenzelm@9138
    96
wenzelm@30641
    97
fun read (syms, pos) =
wenzelm@30641
    98
  (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of
wenzelm@30641
    99
    SOME xs => (List.app (report (K ())) xs; check_nesting xs; xs)
wenzelm@30641
   100
  | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
wenzelm@9138
   101
wenzelm@9138
   102
end;