prefer Name_Space.pretty with its builtin markup;
authorwenzelm
Mon Mar 10 15:20:41 2014 +0100 (2014-03-10)
changeset 5602725889f5c39a8
parent 56026 893fe12639bc
child 56028 422024102d9d
prefer Name_Space.pretty with its builtin markup;
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/try0.ML
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Mar 10 15:04:01 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Mar 10 15:20:41 2014 +0100
     1.3 @@ -162,7 +162,7 @@
     1.4    let
     1.5      val ths = Attrib.eval_thms ctxt [xthm]
     1.6      val bracket =
     1.7 -      map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
     1.8 +      map (enclose "[" "]" o Pretty.str_of o Args.pretty_src Pretty.str ctxt) args
     1.9        |> implode
    1.10      fun nth_name j =
    1.11        (case xref of
     2.1 --- a/src/HOL/Tools/try0.ML	Mon Mar 10 15:04:01 2014 +0100
     2.2 +++ b/src/HOL/Tools/try0.ML	Mon Mar 10 15:20:41 2014 +0100
     2.3 @@ -172,7 +172,7 @@
     2.4  
     2.5  fun string_of_xthm (xref, args) =
     2.6    Facts.string_of_ref xref ^
     2.7 -  implode (map (enclose "[" "]" o Pretty.str_of o Args.pretty_src @{context}) args);
     2.8 +  implode (map (enclose "[" "]" o Pretty.str_of o Args.pretty_src Pretty.str @{context}) args);
     2.9  
    2.10  val parse_fact_refs =
    2.11    Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse_Spec.xthm >> string_of_xthm));
     3.1 --- a/src/Pure/Isar/args.ML	Mon Mar 10 15:04:01 2014 +0100
     3.2 +++ b/src/Pure/Isar/args.ML	Mon Mar 10 15:20:41 2014 +0100
     3.3 @@ -10,7 +10,7 @@
     3.4    type src
     3.5    val src: (string * Token.T list) * Position.T -> src
     3.6    val dest_src: src -> (string * Token.T list) * Position.T
     3.7 -  val pretty_src: Proof.context -> src -> Pretty.T
     3.8 +  val pretty_src: (string -> Pretty.T) -> Proof.context -> src -> Pretty.T
     3.9    val map_name: (string -> string) -> src -> src
    3.10    val transform_values: morphism -> src -> src
    3.11    val init_assignable: src -> src
    3.12 @@ -79,7 +79,7 @@
    3.13  val src = Src;
    3.14  fun dest_src (Src src) = src;
    3.15  
    3.16 -fun pretty_src ctxt src =
    3.17 +fun pretty_src pretty_name ctxt src =
    3.18    let
    3.19      val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
    3.20      fun prt arg =
    3.21 @@ -90,8 +90,8 @@
    3.22        | SOME (Token.Term t) => Syntax.pretty_term ctxt t
    3.23        | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
    3.24        | _ => Pretty.mark_str (Token.markup arg, Token.unparse arg));
    3.25 -    val (s, args) = #1 (dest_src src);
    3.26 -  in Pretty.block (Pretty.breaks (Pretty.str s :: map prt args)) end;
    3.27 +    val (name, args) = #1 (dest_src src);
    3.28 +  in Pretty.block (Pretty.breaks (pretty_name name :: map prt args)) end;
    3.29  
    3.30  fun map_name f (Src ((s, args), pos)) = Src ((f s, args), pos);
    3.31  fun map_args f (Src ((s, args), pos)) = Src ((s, map f args), pos);
     4.1 --- a/src/Pure/Isar/attrib.ML	Mon Mar 10 15:04:01 2014 +0100
     4.2 +++ b/src/Pure/Isar/attrib.ML	Mon Mar 10 15:20:41 2014 +0100
     4.3 @@ -109,6 +109,8 @@
     4.4      |> Pretty.chunks |> Pretty.writeln
     4.5    end;
     4.6  
     4.7 +val attribute_space = Name_Space.space_of_table o get_attributes o Context.Proof;
     4.8 +
     4.9  fun add_attribute name att comment thy = thy
    4.10    |> Attributes.map (Name_Space.define (Context.Theory thy) true (name, (att, comment)) #> snd);
    4.11  
    4.12 @@ -129,12 +131,11 @@
    4.13  
    4.14  (* pretty printing *)
    4.15  
    4.16 -fun extern ctxt =
    4.17 -  Name_Space.extern ctxt (Name_Space.space_of_table (get_attributes (Context.Proof ctxt)));
    4.18 +fun pretty_attrib ctxt =
    4.19 +  Args.pretty_src (Name_Space.pretty ctxt (attribute_space ctxt)) ctxt;
    4.20  
    4.21  fun pretty_attribs _ [] = []
    4.22 -  | pretty_attribs ctxt srcs =
    4.23 -      [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs)];
    4.24 +  | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (pretty_attrib ctxt) srcs)];
    4.25  
    4.26  
    4.27  (* get attributes *)
    4.28 @@ -349,7 +350,7 @@
    4.29          Pretty.block [Pretty.mark_str name, Pretty.str (": " ^ Config.print_type value ^ " ="),
    4.30            Pretty.brk 1, Pretty.str (Config.print_value value)]
    4.31        end;
    4.32 -    val space = Name_Space.space_of_table (get_attributes (Context.Proof ctxt));
    4.33 +    val space = attribute_space ctxt;
    4.34      val configs = Name_Space.extern_table' ctxt space (Configs.get (Proof_Context.theory_of ctxt));
    4.35    in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
    4.36