src/Pure/General/antiquote.ML
author wenzelm
Fri Mar 20 20:21:38 2009 +0100 (2009-03-20)
changeset 30613 b22d35d9ef28
parent 30590 1d9c9fcf8513
child 30635 a7d175c48228
permissions -rw-r--r--
Antiquote.read: argument for reporting text;
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@30590
    11
    Antiq of Symbol_Pos.T list * Position.T |
wenzelm@30590
    12
    Open of Position.T |
wenzelm@30590
    13
    Close of Position.T
wenzelm@30590
    14
  val is_antiq: 'a antiquote -> bool
wenzelm@30590
    15
  val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
wenzelm@30590
    16
  val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
wenzelm@30613
    17
  val read: ('a -> unit) -> (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
wenzelm@30590
    18
    Symbol_Pos.T list * Position.T -> 'a antiquote list
wenzelm@9138
    19
end;
wenzelm@9138
    20
wenzelm@9138
    21
structure Antiquote: ANTIQUOTE =
wenzelm@9138
    22
struct
wenzelm@9138
    23
wenzelm@9138
    24
(* datatype antiquote *)
wenzelm@9138
    25
wenzelm@30590
    26
datatype 'a antiquote =
wenzelm@30590
    27
  Text of 'a |
wenzelm@30573
    28
  Antiq of Symbol_Pos.T list * Position.T |
wenzelm@27342
    29
  Open of Position.T |
wenzelm@27342
    30
  Close of Position.T;
wenzelm@9138
    31
wenzelm@9138
    32
fun is_antiq (Text _) = false
wenzelm@27342
    33
  | is_antiq _ = true;
wenzelm@27342
    34
wenzelm@27342
    35
wenzelm@27342
    36
(* check_nesting *)
wenzelm@27342
    37
wenzelm@27342
    38
fun err_unbalanced pos =
wenzelm@27342
    39
  error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos);
wenzelm@27342
    40
wenzelm@27342
    41
fun check_nesting antiqs =
wenzelm@27342
    42
  let
wenzelm@27342
    43
    fun check [] [] = ()
wenzelm@27342
    44
      | check [] (pos :: _) = err_unbalanced pos
wenzelm@27342
    45
      | check (Open pos :: ants) ps = check ants (pos :: ps)
wenzelm@27342
    46
      | check (Close pos :: _) [] = err_unbalanced pos
wenzelm@27342
    47
      | check (Close _ :: ants) (_ :: ps) = check ants ps
wenzelm@27342
    48
      | check (_ :: ants) ps = check ants ps;
wenzelm@27342
    49
  in check antiqs [] end;
wenzelm@9138
    50
wenzelm@9138
    51
wenzelm@30590
    52
(* scan *)
wenzelm@9138
    53
wenzelm@30573
    54
open Basic_Symbol_Pos;
wenzelm@9138
    55
wenzelm@22114
    56
local
wenzelm@9138
    57
wenzelm@9138
    58
val scan_txt =
wenzelm@27767
    59
  $$$ "@" --| Scan.ahead (~$$$ "{") ||
wenzelm@27767
    60
  Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
wenzelm@27767
    61
    andalso Symbol.is_regular s) >> single;
wenzelm@9138
    62
wenzelm@9138
    63
val scan_ant =
wenzelm@30587
    64
  Symbol_Pos.scan_quoted ||
wenzelm@27767
    65
  Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
wenzelm@9138
    66
wenzelm@9138
    67
val scan_antiq =
wenzelm@30573
    68
  Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
wenzelm@30587
    69
    Symbol_Pos.!!! "missing closing brace of antiquotation"
wenzelm@30573
    70
      (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
wenzelm@30590
    71
  >> (fn (pos1, (body, pos2)) => (flat body, Position.encode_range (pos1, pos2)));
wenzelm@30590
    72
wenzelm@30590
    73
val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
wenzelm@30590
    74
val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>";
wenzelm@9138
    75
wenzelm@9138
    76
in
wenzelm@9138
    77
wenzelm@30590
    78
fun scan x = (scan_antiq >> Antiq || scan_open >> Open || scan_close >> Close) x;
wenzelm@30590
    79
val scan_text = scan || Scan.repeat1 scan_txt >> (Text o flat);
wenzelm@9138
    80
wenzelm@9138
    81
end;
wenzelm@9138
    82
wenzelm@9138
    83
wenzelm@27767
    84
(* read *)
wenzelm@9138
    85
wenzelm@30613
    86
fun read _ _ ([], _) = []
wenzelm@30613
    87
  | read report scanner (syms, pos) =
wenzelm@30590
    88
      (case Scan.read Symbol_Pos.stopper (Scan.repeat scanner) syms of
wenzelm@30613
    89
        SOME xs =>
wenzelm@30613
    90
         (List.app (fn Antiq (_, pos) => Position.report Markup.antiq pos | Text x => report x) xs;
wenzelm@30613
    91
          check_nesting xs; xs)
wenzelm@27767
    92
      | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
wenzelm@9138
    93
wenzelm@9138
    94
end;