src/Pure/Isar/antiquote.ML
author wenzelm
Wed Mar 18 21:55:38 2009 +0100 (2009-03-18)
changeset 30573 49899f26fbd1
parent 29606 fedb8be05f24
permissions -rw-r--r--
de-camelized Symbol_Pos;
wenzelm@9138
     1
(*  Title:      Pure/Isar/antiquote.ML
wenzelm@9138
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@9138
     3
wenzelm@9138
     4
Text with antiquotations of inner items (terms, types etc.).
wenzelm@9138
     5
*)
wenzelm@9138
     6
wenzelm@9138
     7
signature ANTIQUOTE =
wenzelm@9138
     8
sig
wenzelm@27342
     9
  datatype antiquote =
wenzelm@30573
    10
    Text of string | 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@27779
    14
  val read_antiq: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) ->
wenzelm@30573
    15
    Symbol_Pos.T list * Position.T -> 'a
wenzelm@9138
    16
end;
wenzelm@9138
    17
wenzelm@9138
    18
structure Antiquote: ANTIQUOTE =
wenzelm@9138
    19
struct
wenzelm@9138
    20
wenzelm@9138
    21
(* datatype antiquote *)
wenzelm@9138
    22
wenzelm@9138
    23
datatype antiquote =
wenzelm@9138
    24
  Text of string |
wenzelm@30573
    25
  Antiq of Symbol_Pos.T list * Position.T |
wenzelm@27342
    26
  Open of Position.T |
wenzelm@27342
    27
  Close of Position.T;
wenzelm@9138
    28
wenzelm@9138
    29
fun is_antiq (Text _) = false
wenzelm@27342
    30
  | is_antiq _ = true;
wenzelm@27342
    31
wenzelm@27342
    32
wenzelm@27342
    33
(* check_nesting *)
wenzelm@27342
    34
wenzelm@27342
    35
fun err_unbalanced pos =
wenzelm@27342
    36
  error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos);
wenzelm@27342
    37
wenzelm@27342
    38
fun check_nesting antiqs =
wenzelm@27342
    39
  let
wenzelm@27342
    40
    fun check [] [] = ()
wenzelm@27342
    41
      | check [] (pos :: _) = err_unbalanced pos
wenzelm@27342
    42
      | check (Open pos :: ants) ps = check ants (pos :: ps)
wenzelm@27342
    43
      | check (Close pos :: _) [] = err_unbalanced pos
wenzelm@27342
    44
      | check (Close _ :: ants) (_ :: ps) = check ants ps
wenzelm@27342
    45
      | check (_ :: ants) ps = check ants ps;
wenzelm@27342
    46
  in check antiqs [] end;
wenzelm@9138
    47
wenzelm@9138
    48
wenzelm@9138
    49
(* scan_antiquote *)
wenzelm@9138
    50
wenzelm@30573
    51
open Basic_Symbol_Pos;
wenzelm@22114
    52
structure T = OuterLex;
wenzelm@9138
    53
wenzelm@22114
    54
local
wenzelm@9138
    55
wenzelm@9138
    56
val scan_txt =
wenzelm@27767
    57
  $$$ "@" --| Scan.ahead (~$$$ "{") ||
wenzelm@27767
    58
  Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
wenzelm@27767
    59
    andalso Symbol.is_regular s) >> single;
wenzelm@9138
    60
wenzelm@9138
    61
val scan_ant =
wenzelm@27767
    62
  T.scan_quoted ||
wenzelm@27767
    63
  Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
wenzelm@9138
    64
wenzelm@9138
    65
val scan_antiq =
wenzelm@30573
    66
  Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
wenzelm@9138
    67
    T.!!! "missing closing brace of antiquotation"
wenzelm@30573
    68
      (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
wenzelm@27870
    69
  >> (fn (pos1, (body, pos2)) => Antiq (flat body, Position.encode_range (pos1, pos2)));
wenzelm@9138
    70
wenzelm@9138
    71
in
wenzelm@9138
    72
wenzelm@27779
    73
val scan_antiquote =
wenzelm@30573
    74
 (Scan.repeat1 scan_txt >> (Text o Symbol_Pos.content o flat) ||
wenzelm@27750
    75
  scan_antiq ||
wenzelm@30573
    76
  Symbol_Pos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
wenzelm@30573
    77
  Symbol_Pos.scan_pos --| $$$ "\\<rbrace>" >> Close);
wenzelm@9138
    78
wenzelm@9138
    79
end;
wenzelm@9138
    80
wenzelm@9138
    81
wenzelm@27767
    82
(* read *)
wenzelm@9138
    83
wenzelm@27880
    84
fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
wenzelm@27880
    85
  | report_antiq _ = ();
wenzelm@27880
    86
wenzelm@27870
    87
fun read ([], _) = []
wenzelm@27870
    88
  | read (syms, pos) =
wenzelm@30573
    89
      (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
wenzelm@27880
    90
        SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
wenzelm@27767
    91
      | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
wenzelm@9138
    92
wenzelm@9138
    93
wenzelm@27779
    94
(* read_antiq *)
wenzelm@22114
    95
wenzelm@27870
    96
fun read_antiq lex scan (syms, pos) =
wenzelm@22114
    97
  let
wenzelm@27870
    98
    fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
wenzelm@30573
    99
      "@{" ^ Symbol_Pos.content syms ^ "}");
wenzelm@22114
   100
wenzelm@22114
   101
    val res =
wenzelm@27870
   102
      Source.of_list syms
wenzelm@27835
   103
      |> T.source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
wenzelm@22114
   104
      |> T.source_proper
wenzelm@27767
   105
      |> Source.source T.stopper (Scan.error (Scan.bulk scan)) NONE
wenzelm@22114
   106
      |> Source.exhaust;
wenzelm@22114
   107
  in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
wenzelm@22114
   108
wenzelm@9138
   109
end;