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