src/Pure/Isar/antiquote.ML
author wenzelm
Sun Jun 25 23:56:47 2000 +0200 (2000-06-25)
changeset 9138 6a4fae41a75f
child 12881 eeb36b66480e
permissions -rw-r--r--
Text with antiquotations of inner items (terms, types etc.).
wenzelm@9138
     1
(*  Title:      Pure/Isar/antiquote.ML
wenzelm@9138
     2
    ID:         $Id$
wenzelm@9138
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@9138
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@9138
     5
wenzelm@9138
     6
Text with antiquotations of inner items (terms, types etc.).
wenzelm@9138
     7
*)
wenzelm@9138
     8
wenzelm@9138
     9
signature ANTIQUOTE =
wenzelm@9138
    10
sig
wenzelm@9138
    11
  datatype antiquote = Text of string | Antiq of string * Position.T
wenzelm@9138
    12
  val is_antiq: antiquote -> bool
wenzelm@9138
    13
  val antiquotes_of: string * 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@9138
    22
  Text of string |
wenzelm@9138
    23
  Antiq of string * Position.T;
wenzelm@9138
    24
wenzelm@9138
    25
fun is_antiq (Text _) = false
wenzelm@9138
    26
  | is_antiq (Antiq _) = true;
wenzelm@9138
    27
wenzelm@9138
    28
wenzelm@9138
    29
(* scan_antiquote *)
wenzelm@9138
    30
wenzelm@9138
    31
local
wenzelm@9138
    32
wenzelm@9138
    33
structure T = OuterLex;
wenzelm@9138
    34
wenzelm@9138
    35
val scan_txt =
wenzelm@9138
    36
  T.scan_blank ||
wenzelm@9138
    37
  T.keep_line ($$ "@" --| Scan.ahead (Scan.one (not_equal "{"))) ||
wenzelm@9138
    38
  T.keep_line (Scan.one (not_equal "@" andf Symbol.not_sync andf Symbol.not_eof));
wenzelm@9138
    39
wenzelm@9138
    40
fun escape "\\" = "\\\\"
wenzelm@9138
    41
  | escape "\"" = "\\\""
wenzelm@9138
    42
  | escape s = s;
wenzelm@9138
    43
wenzelm@9138
    44
val quote_escape = quote o implode o map escape o Symbol.explode;
wenzelm@9138
    45
wenzelm@9138
    46
val scan_ant =
wenzelm@9138
    47
  T.scan_blank ||
wenzelm@9138
    48
  T.scan_string >> quote_escape ||
wenzelm@9138
    49
  T.keep_line (Scan.one (not_equal "}" andf Symbol.not_sync andf Symbol.not_eof));
wenzelm@9138
    50
wenzelm@9138
    51
val scan_antiq =
wenzelm@9138
    52
  T.keep_line ($$ "@" -- $$ "{") |--
wenzelm@9138
    53
    T.!!! "missing closing brace of antiquotation"
wenzelm@9138
    54
      (Scan.repeat scan_ant >> implode) --| T.keep_line ($$ "}");
wenzelm@9138
    55
wenzelm@9138
    56
in
wenzelm@9138
    57
wenzelm@9138
    58
fun scan_antiquote (pos, ss) = (pos, ss) |>
wenzelm@9138
    59
  (Scan.repeat1 scan_txt >> (Text o implode) ||
wenzelm@9138
    60
    scan_antiq >> (fn s => Antiq (s, pos)));
wenzelm@9138
    61
wenzelm@9138
    62
end;
wenzelm@9138
    63
wenzelm@9138
    64
wenzelm@9138
    65
(* antiquotes_of *)
wenzelm@9138
    66
wenzelm@9138
    67
fun antiquotes_of (s, pos) =
wenzelm@9138
    68
  (case Scan.error (Scan.finite' Symbol.stopper (Scan.repeat scan_antiquote))
wenzelm@9138
    69
      (pos, Symbol.explode s) of
wenzelm@9138
    70
    (xs, (_, [])) => xs
wenzelm@9138
    71
  | (_, (pos', ss)) => error ("Malformed quotation/antiquotation text at: " ^
wenzelm@9138
    72
      quote (Symbol.beginning ss) ^ Position.str_of pos'));
wenzelm@9138
    73
wenzelm@9138
    74
wenzelm@9138
    75
end;