replaced Antiquote.is_antiq by Antiquote.is_text;
authorwenzelm
Sun, 22 Mar 2009 19:10:58 +0100
changeset 30635 a7d175c48228
parent 30634 bc3c1b7df4ec
child 30636 bd8813d7774d
replaced Antiquote.is_antiq by Antiquote.is_text;
src/Pure/General/antiquote.ML
src/Pure/Thy/thy_output.ML
--- 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;