Antiquote.read: argument for reporting text;
authorwenzelm
Fri Mar 20 20:21:38 2009 +0100 (2009-03-20 ago)
changeset 30613b22d35d9ef28
parent 30612 cb6421b6a18f
child 30614 845bcfd3e9cd
Antiquote.read: argument for reporting text;
src/Pure/General/antiquote.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/General/antiquote.ML	Fri Mar 20 20:20:09 2009 +0100
     1.2 +++ b/src/Pure/General/antiquote.ML	Fri Mar 20 20:21:38 2009 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4    val is_antiq: 'a antiquote -> bool
     1.5    val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
     1.6    val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
     1.7 -  val read: (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
     1.8 +  val read: ('a -> unit) -> (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
     1.9      Symbol_Pos.T list * Position.T -> 'a antiquote list
    1.10  end;
    1.11  
    1.12 @@ -83,13 +83,12 @@
    1.13  
    1.14  (* read *)
    1.15  
    1.16 -fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
    1.17 -  | report_antiq _ = ();
    1.18 -
    1.19 -fun read _ ([], _) = []
    1.20 -  | read scanner (syms, pos) =
    1.21 +fun read _ _ ([], _) = []
    1.22 +  | read report scanner (syms, pos) =
    1.23        (case Scan.read Symbol_Pos.stopper (Scan.repeat scanner) syms of
    1.24 -        SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
    1.25 +        SOME xs =>
    1.26 +         (List.app (fn Antiq (_, pos) => Position.report Markup.antiq pos | Text x => report x) xs;
    1.27 +          check_nesting xs; xs)
    1.28        | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
    1.29  
    1.30  end;
     2.1 --- a/src/Pure/Thy/latex.ML	Fri Mar 20 20:20:09 2009 +0100
     2.2 +++ b/src/Pure/Thy/latex.ML	Fri Mar 20 20:21:38 2009 +0100
     2.3 @@ -117,7 +117,7 @@
     2.4      else if T.is_kind T.Verbatim tok then
     2.5        let
     2.6          val (txt, pos) = T.source_position_of tok;
     2.7 -        val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
     2.8 +        val ants = Antiquote.read (K ()) Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
     2.9          val out = implode (map output_syms_antiq ants);
    2.10        in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
    2.11      else output_syms s
     3.1 --- a/src/Pure/Thy/thy_output.ML	Fri Mar 20 20:20:09 2009 +0100
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Mar 20 20:21:38 2009 +0100
     3.3 @@ -156,7 +156,7 @@
     3.4            end
     3.5        | expand (Antiquote.Open _) = ""
     3.6        | expand (Antiquote.Close _) = "";
     3.7 -    val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
     3.8 +    val ants = Antiquote.read (K ()) Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
     3.9    in
    3.10      if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
    3.11        error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)