tuned;
authorwenzelm
Tue Nov 18 18:25:45 2008 +0100 (2008-11-18)
changeset 28840049f0a8faa35
parent 28839 32d498cf7595
child 28841 5556c7976837
tuned;
src/Pure/Syntax/syntax.ML
src/Pure/Thy/html.ML
src/Pure/Thy/present.ML
src/Pure/display.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Tue Nov 18 18:25:42 2008 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Nov 18 18:25:45 2008 +0100
     1.3 @@ -400,7 +400,7 @@
     1.4  local
     1.5  
     1.6  fun pretty_strs_qs name strs =
     1.7 -  Pretty.strs (name :: map Library.quote (sort_strings strs));
     1.8 +  Pretty.strs (name :: map quote (sort_strings strs));
     1.9  
    1.10  fun pretty_gram (Syntax (tabs, _)) =
    1.11    let
    1.12 @@ -420,7 +420,7 @@
    1.13      fun pretty_ruletab name tab =
    1.14        Pretty.big_list name (map Ast.pretty_rule (dest_ruletab tab));
    1.15  
    1.16 -    fun pretty_tokentr (mode, trs) = Pretty.strs (Library.quote mode ^ ":" :: map fst trs);
    1.17 +    fun pretty_tokentr (mode, trs) = Pretty.strs (quote mode ^ ":" :: map fst trs);
    1.18  
    1.19      val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab,
    1.20        print_ruletab, print_ast_trtab, tokentrtab, ...} = tabs;
     2.1 --- a/src/Pure/Thy/html.ML	Tue Nov 18 18:25:42 2008 +0100
     2.2 +++ b/src/Pure/Thy/html.ML	Tue Nov 18 18:25:45 2008 +0100
     2.3 @@ -232,7 +232,7 @@
     2.4  
     2.5  (* common markup *)
     2.6  
     2.7 -fun span s = ("<span class=" ^ Library.quote (XML.text s) ^ ">", "</span>");
     2.8 +fun span s = ("<span class=" ^ quote (XML.text s) ^ ">", "</span>");
     2.9  
    2.10  val _ = Markup.add_mode htmlN (fn (name, _) => span name);
    2.11  
    2.12 @@ -255,7 +255,7 @@
    2.13  
    2.14  (* misc *)
    2.15  
    2.16 -fun href_name s txt = "<a href=" ^ Library.quote s ^ ">" ^ txt ^ "</a>";
    2.17 +fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>";
    2.18  fun href_path path txt = href_name (Url.implode path) txt;
    2.19  
    2.20  fun href_opt_path NONE txt = txt
     3.1 --- a/src/Pure/Thy/present.ML	Tue Nov 18 18:25:42 2008 +0100
     3.2 +++ b/src/Pure/Thy/present.ML	Tue Nov 18 18:25:45 2008 +0100
     3.3 @@ -89,7 +89,7 @@
     3.4  fun write_graph gr path =
     3.5    File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
     3.6      "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
     3.7 -    path ^ "\" > " ^ space_implode " " (map Library.quote parents) ^ " ;") gr));
     3.8 +    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
     3.9  
    3.10  fun display_graph gr =
    3.11    let
     4.1 --- a/src/Pure/display.ML	Tue Nov 18 18:25:42 2008 +0100
     4.2 +++ b/src/Pure/display.ML	Tue Nov 18 18:25:45 2008 +0100
     4.3 @@ -52,7 +52,7 @@
     4.4  val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
     4.5  val show_tags = ref false;      (*false: suppress tags*)
     4.6  
     4.7 -fun pretty_tag (name, arg) = Pretty.strs [name, Library.quote arg];
     4.8 +fun pretty_tag (name, arg) = Pretty.strs [name, quote arg];
     4.9  val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    4.10  
    4.11  fun pretty_flexpair pp (t, u) = Pretty.block