src/Pure/General/antiquote.ML
changeset 30587 ad19c99529eb
parent 30573 49899f26fbd1
child 30589 cbe27c4ef417
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/antiquote.ML	Thu Mar 19 15:22:53 2009 +0100
     1.3 @@ -0,0 +1,90 @@
     1.4 +(*  Title:      Pure/General/antiquote.ML
     1.5 +    Author:     Markus Wenzel, TU Muenchen
     1.6 +
     1.7 +Text with antiquotations of inner items (types, terms, theorems etc.).
     1.8 +*)
     1.9 +
    1.10 +signature ANTIQUOTE =
    1.11 +sig
    1.12 +  datatype antiquote =
    1.13 +    Text of string | Antiq of Symbol_Pos.T list * Position.T |
    1.14 +    Open of Position.T | Close of Position.T
    1.15 +  val is_antiq: antiquote -> bool
    1.16 +  val read: Symbol_Pos.T list * Position.T -> antiquote list
    1.17 +end;
    1.18 +
    1.19 +structure Antiquote: ANTIQUOTE =
    1.20 +struct
    1.21 +
    1.22 +(* datatype antiquote *)
    1.23 +
    1.24 +datatype antiquote =
    1.25 +  Text of string |
    1.26 +  Antiq of Symbol_Pos.T list * Position.T |
    1.27 +  Open of Position.T |
    1.28 +  Close of Position.T;
    1.29 +
    1.30 +fun is_antiq (Text _) = false
    1.31 +  | is_antiq _ = true;
    1.32 +
    1.33 +
    1.34 +(* check_nesting *)
    1.35 +
    1.36 +fun err_unbalanced pos =
    1.37 +  error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos);
    1.38 +
    1.39 +fun check_nesting antiqs =
    1.40 +  let
    1.41 +    fun check [] [] = ()
    1.42 +      | check [] (pos :: _) = err_unbalanced pos
    1.43 +      | check (Open pos :: ants) ps = check ants (pos :: ps)
    1.44 +      | check (Close pos :: _) [] = err_unbalanced pos
    1.45 +      | check (Close _ :: ants) (_ :: ps) = check ants ps
    1.46 +      | check (_ :: ants) ps = check ants ps;
    1.47 +  in check antiqs [] end;
    1.48 +
    1.49 +
    1.50 +(* scan_antiquote *)
    1.51 +
    1.52 +open Basic_Symbol_Pos;
    1.53 +
    1.54 +local
    1.55 +
    1.56 +val scan_txt =
    1.57 +  $$$ "@" --| Scan.ahead (~$$$ "{") ||
    1.58 +  Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
    1.59 +    andalso Symbol.is_regular s) >> single;
    1.60 +
    1.61 +val scan_ant =
    1.62 +  Symbol_Pos.scan_quoted ||
    1.63 +  Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
    1.64 +
    1.65 +val scan_antiq =
    1.66 +  Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
    1.67 +    Symbol_Pos.!!! "missing closing brace of antiquotation"
    1.68 +      (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
    1.69 +  >> (fn (pos1, (body, pos2)) => Antiq (flat body, Position.encode_range (pos1, pos2)));
    1.70 +
    1.71 +in
    1.72 +
    1.73 +val scan_antiquote =
    1.74 + (Scan.repeat1 scan_txt >> (Text o Symbol_Pos.content o flat) ||
    1.75 +  scan_antiq ||
    1.76 +  Symbol_Pos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
    1.77 +  Symbol_Pos.scan_pos --| $$$ "\\<rbrace>" >> Close);
    1.78 +
    1.79 +end;
    1.80 +
    1.81 +
    1.82 +(* read *)
    1.83 +
    1.84 +fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
    1.85 +  | report_antiq _ = ();
    1.86 +
    1.87 +fun read ([], _) = []
    1.88 +  | read (syms, pos) =
    1.89 +      (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
    1.90 +        SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
    1.91 +      | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
    1.92 +
    1.93 +end;