src/Pure/Isar/antiquote.ML
author wenzelm
Tue Dec 05 22:14:42 2006 +0100 (2006-12-05)
changeset 21658 5e31241e1e3c
parent 19305 5c16895d548b
child 22114 560c5b5dda1c
permissions -rw-r--r--
Attrib.internal: morphism;
wenzelm@9138
     1
(*  Title:      Pure/Isar/antiquote.ML
wenzelm@9138
     2
    ID:         $Id$
wenzelm@9138
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@9138
     4
wenzelm@9138
     5
Text with antiquotations of inner items (terms, types etc.).
wenzelm@9138
     6
*)
wenzelm@9138
     7
wenzelm@9138
     8
signature ANTIQUOTE =
wenzelm@9138
     9
sig
wenzelm@12881
    10
  exception ANTIQUOTE_FAIL of (string * Position.T) * exn
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@12881
    21
exception ANTIQUOTE_FAIL of (string * Position.T) * exn;
wenzelm@12881
    22
wenzelm@9138
    23
datatype antiquote =
wenzelm@9138
    24
  Text of string |
wenzelm@9138
    25
  Antiq of string * Position.T;
wenzelm@9138
    26
wenzelm@9138
    27
fun is_antiq (Text _) = false
wenzelm@9138
    28
  | is_antiq (Antiq _) = true;
wenzelm@9138
    29
wenzelm@9138
    30
wenzelm@9138
    31
(* scan_antiquote *)
wenzelm@9138
    32
wenzelm@9138
    33
local
wenzelm@9138
    34
wenzelm@9138
    35
structure T = OuterLex;
wenzelm@9138
    36
wenzelm@9138
    37
val scan_txt =
wenzelm@9138
    38
  T.scan_blank ||
wenzelm@19305
    39
  T.keep_line ($$ "@" --| Scan.ahead (~$$ "{")) ||
wenzelm@19305
    40
  T.keep_line (Scan.one (fn s => s <> "@" andalso Symbol.not_sync s andalso Symbol.not_eof s));
wenzelm@9138
    41
wenzelm@9138
    42
fun escape "\\" = "\\\\"
wenzelm@9138
    43
  | escape "\"" = "\\\""
wenzelm@9138
    44
  | escape s = s;
wenzelm@9138
    45
berghofe@14598
    46
val quote_escape = Library.quote o implode o map escape o Symbol.explode;
wenzelm@9138
    47
wenzelm@9138
    48
val scan_ant =
wenzelm@9138
    49
  T.scan_blank ||
wenzelm@9138
    50
  T.scan_string >> quote_escape ||
wenzelm@19305
    51
  T.keep_line (Scan.one (fn s => s <> "}" andalso Symbol.not_sync s andalso Symbol.not_eof s));
wenzelm@9138
    52
wenzelm@9138
    53
val scan_antiq =
wenzelm@9138
    54
  T.keep_line ($$ "@" -- $$ "{") |--
wenzelm@9138
    55
    T.!!! "missing closing brace of antiquotation"
wenzelm@9138
    56
      (Scan.repeat scan_ant >> implode) --| T.keep_line ($$ "}");
wenzelm@9138
    57
wenzelm@9138
    58
in
wenzelm@9138
    59
wenzelm@9138
    60
fun scan_antiquote (pos, ss) = (pos, ss) |>
wenzelm@9138
    61
  (Scan.repeat1 scan_txt >> (Text o implode) ||
wenzelm@9138
    62
    scan_antiq >> (fn s => Antiq (s, pos)));
wenzelm@9138
    63
wenzelm@9138
    64
end;
wenzelm@9138
    65
wenzelm@9138
    66
wenzelm@9138
    67
(* antiquotes_of *)
wenzelm@9138
    68
wenzelm@9138
    69
fun antiquotes_of (s, pos) =
wenzelm@9138
    70
  (case Scan.error (Scan.finite' Symbol.stopper (Scan.repeat scan_antiquote))
wenzelm@9138
    71
      (pos, Symbol.explode s) of
wenzelm@9138
    72
    (xs, (_, [])) => xs
wenzelm@9138
    73
  | (_, (pos', ss)) => error ("Malformed quotation/antiquotation text at: " ^
wenzelm@14729
    74
      quote (Symbol.beginning 10 ss) ^ Position.str_of pos'));
wenzelm@9138
    75
wenzelm@9138
    76
wenzelm@9138
    77
end;