--- a/src/Pure/General/antiquote.ML Sat Mar 21 20:39:38 2009 +0100
+++ b/src/Pure/General/antiquote.ML Sun Mar 22 19:10:58 2009 +0100
@@ -11,7 +11,7 @@
Antiq of Symbol_Pos.T list * Position.T |
Open of Position.T |
Close of Position.T
- val is_antiq: 'a antiquote -> bool
+ val is_text: 'a antiquote -> bool
val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
val read: ('a -> unit) -> (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
@@ -29,8 +29,8 @@
Open of Position.T |
Close of Position.T;
-fun is_antiq (Text _) = false
- | is_antiq _ = true;
+fun is_text (Text _) = true
+ | is_text _ = false;
(* check_nesting *)
--- a/src/Pure/Thy/thy_output.ML Sat Mar 21 20:39:38 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML Sun Mar 22 19:10:58 2009 +0100
@@ -158,7 +158,7 @@
| expand (Antiquote.Close _) = "";
val ants = Antiquote.read (K ()) Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
in
- if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
+ if Toplevel.is_toplevel state andalso not (forall Antiquote.is_text ants) then
error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
else implode (map expand ants)
end;