report antiquotation names;
authorwenzelm
Fri Aug 15 17:03:58 2008 +0200 (2008-08-15)
changeset 278970e7ff439460f
parent 27896 220e7a18a8ea
child 27898 e0953043ce90
report antiquotation names;
tuned messages;
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Thy/thy_output.ML	Fri Aug 15 17:03:56 2008 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Aug 15 17:03:58 2008 +0200
     1.3 @@ -60,7 +60,7 @@
     1.4  
     1.5  fun add_item kind (name, x) tab =
     1.6   (if not (Symtab.defined tab name) then ()
     1.7 -  else warning ("Redefined text antiquotation " ^ kind ^ ": " ^ quote name);
     1.8 +  else warning ("Redefined document antiquotation " ^ kind ^ ": " ^ quote name);
     1.9    Symtab.update (name, x) tab);
    1.10  
    1.11  in
    1.12 @@ -74,13 +74,13 @@
    1.13  fun command src =
    1.14    let val ((name, _), pos) = Args.dest_src src in
    1.15      (case Symtab.lookup (! global_commands) name of
    1.16 -      NONE => error ("Unknown text antiquotation command: " ^ quote name ^ Position.str_of pos)
    1.17 -    | SOME f => f src)
    1.18 +      NONE => error ("Unknown document antiquotation command: " ^ quote name ^ Position.str_of pos)
    1.19 +    | SOME f => (Position.report (Markup.doc_antiq name) pos; f src))
    1.20    end;
    1.21  
    1.22  fun option (name, s) f () =
    1.23    (case Symtab.lookup (! global_options) name of
    1.24 -    NONE => error ("Unknown text antiquotation option: " ^ quote name)
    1.25 +    NONE => error ("Unknown document antiquotation option: " ^ quote name)
    1.26    | SOME opt => opt s f ());
    1.27  
    1.28  fun options [] f = f
    1.29 @@ -88,9 +88,9 @@
    1.30  
    1.31  
    1.32  fun print_antiquotations () =
    1.33 - [Pretty.big_list "text antiquotation commands:"
    1.34 + [Pretty.big_list "document antiquotation commands:"
    1.35      (map Pretty.str (sort_strings (Symtab.keys (! global_commands)))),
    1.36 -  Pretty.big_list "text antiquotation options:"
    1.37 +  Pretty.big_list "document antiquotation options:"
    1.38      (map Pretty.str (sort_strings (Symtab.keys (! global_options))))]
    1.39   |> Pretty.chunks |> Pretty.writeln;
    1.40  
    1.41 @@ -117,7 +117,7 @@
    1.42  
    1.43  (* args syntax *)
    1.44  
    1.45 -fun syntax scan = Args.context_syntax "text antiquotation" scan;
    1.46 +fun syntax scan = Args.context_syntax "document antiquotation" scan;
    1.47  
    1.48  fun args scan f src node : string =
    1.49    let
    1.50 @@ -159,7 +159,7 @@
    1.51      val ants = Antiquote.read (SymbolPos.explode (txt, pos), pos);
    1.52    in
    1.53      if is_none node andalso exists Antiquote.is_antiq ants then
    1.54 -      error ("Unknown context -- cannot expand text antiquotations" ^ Position.str_of pos)
    1.55 +      error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
    1.56      else implode (map expand ants)
    1.57    end;
    1.58