replaced Antiquote.is_antiq by Antiquote.is_text;
authorwenzelm
Sun Mar 22 19:10:58 2009 +0100 (2009-03-22)
changeset 30635a7d175c48228
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
     1.1 --- a/src/Pure/General/antiquote.ML	Sat Mar 21 20:39:38 2009 +0100
     1.2 +++ b/src/Pure/General/antiquote.ML	Sun Mar 22 19:10:58 2009 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4      Antiq of Symbol_Pos.T list * Position.T |
     1.5      Open of Position.T |
     1.6      Close of Position.T
     1.7 -  val is_antiq: 'a antiquote -> bool
     1.8 +  val is_text: 'a antiquote -> bool
     1.9    val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
    1.10    val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
    1.11    val read: ('a -> unit) -> (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
    1.12 @@ -29,8 +29,8 @@
    1.13    Open of Position.T |
    1.14    Close of Position.T;
    1.15  
    1.16 -fun is_antiq (Text _) = false
    1.17 -  | is_antiq _ = true;
    1.18 +fun is_text (Text _) = true
    1.19 +  | is_text _ = false;
    1.20  
    1.21  
    1.22  (* check_nesting *)
     2.1 --- a/src/Pure/Thy/thy_output.ML	Sat Mar 21 20:39:38 2009 +0100
     2.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Mar 22 19:10:58 2009 +0100
     2.3 @@ -158,7 +158,7 @@
     2.4        | expand (Antiquote.Close _) = "";
     2.5      val ants = Antiquote.read (K ()) Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
     2.6    in
     2.7 -    if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
     2.8 +    if Toplevel.is_toplevel state andalso not (forall Antiquote.is_text ants) then
     2.9        error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
    2.10      else implode (map expand ants)
    2.11    end;