Replaced quote by Library.quote, since quote now refers to Symbol.quote
authorberghofe
Fri Apr 16 18:45:56 2004 +0200 (2004-04-16)
changeset 145987009f59711e3
parent 14597 ee0fb03f5f1e
child 14599 c3177fffd31a
Replaced quote by Library.quote, since quote now refers to Symbol.quote
src/HOL/thy_syntax.ML
src/Pure/Isar/antiquote.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Syntax/syntax.ML
src/Pure/Thy/html.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/present.ML
src/Pure/Thy/thy_parse.ML
src/Pure/codegen.ML
src/Pure/display.ML
src/ZF/thy_syntax.ML
     1.1 --- a/src/HOL/thy_syntax.ML	Fri Apr 16 18:44:39 2004 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Fri Apr 16 18:45:56 2004 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4      fun mk_params ((recs, ipairs), monos) =
     1.5        let val big_rec_name = space_implode "_" (map (scan_to_id o unenclose) recs)
     1.6            and srec_tms = mk_list recs
     1.7 -          and sintrs   = mk_big_list (no_atts (map (mk_pair o apfst quote) ipairs))
     1.8 +          and sintrs   = mk_big_list (no_atts (map (mk_pair o apfst Library.quote) ipairs))
     1.9        in
    1.10          ";\n\n\
    1.11          \local\n\
    1.12 @@ -133,7 +133,7 @@
    1.13        val names = map (fn ((((alt_name, _), name), _), _) =>
    1.14          unenclose (if_none alt_name name)) dts;
    1.15  
    1.16 -      val add_datatype_args = brackets (commas (map quote names)) ^ " " ^
    1.17 +      val add_datatype_args = brackets (commas (map Library.quote names)) ^ " " ^
    1.18          brackets (commas (map (fn ((((_, vs), name), mx), cs) =>
    1.19            parens (brackets (commas vs) ^ ", " ^ name ^ ", " ^ mx ^ ", " ^
    1.20              brackets (commas cs))) dts));
    1.21 @@ -156,7 +156,7 @@
    1.22      \  case_thms, split_thms, induction, size, simps}) =\n\
    1.23      \ DatatypePackage.rep_datatype " ^
    1.24      (case names of
    1.25 -        Some names => "(Some [" ^ commas_quote names ^ "])\n " ^
    1.26 +        Some names => "(Some [" ^ Library.commas_quote names ^ "])\n " ^
    1.27            mk_thmss distinct ^ "\n " ^ mk_thmss inject ^
    1.28              "\n " ^ mk_thm induct ^ " thy;\nin\n" ^ mk_bind_thms_string names
    1.29        | None => "None\n " ^ mk_thmss distinct ^ "\n " ^ mk_thmss inject ^
    1.30 @@ -179,7 +179,7 @@
    1.31    val opt_typs = repeat ((string >> unenclose) ||
    1.32      simple_typ || ("(" $$-- complex_typ --$$ ")"));
    1.33    val constructor = name -- opt_typs -- opt_mixfix >> (fn ((n, Ts), mx) =>
    1.34 -    parens (n ^ ", " ^ brackets (commas_quote Ts) ^ ", " ^ mx));
    1.35 +    parens (n ^ ", " ^ brackets (Library.commas_quote Ts) ^ ", " ^ mx));
    1.36    val opt_name = optional ("(" $$-- name --$$ ")" >> Some) None
    1.37  
    1.38    fun optlistlist s = optional (s $$-- enum "and" (list name)) [[]]
    1.39 @@ -199,7 +199,7 @@
    1.40  (** primrec **)
    1.41  
    1.42  fun mk_patterns eqns = mk_list (map (fn (s, _) => if s = "" then "_" else s) eqns);
    1.43 -fun mk_eqns eqns = mk_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) eqns);
    1.44 +fun mk_eqns eqns = mk_list (map (fn (x, y) => mk_pair (mk_pair (Library.quote x, y), "[]")) eqns);
    1.45  
    1.46  fun mk_primrec_decl (alt_name, eqns) =
    1.47    ";\nval (thy, " ^ mk_patterns eqns ^ ") = PrimrecPackage.add_primrec " ^ alt_name ^ " "
    1.48 @@ -221,7 +221,7 @@
    1.49      ";\n\n\
    1.50      \local\n\
    1.51      \fun simpset() = Simplifier.simpset_of thy;\n\
    1.52 -    \val (thy, result) = thy |> RecdefPackage.add_recdef_old " ^ quote fid ^ " " ^ rel ^ "\n" ^
    1.53 +    \val (thy, result) = thy |> RecdefPackage.add_recdef_old " ^ Library.quote fid ^ " " ^ rel ^ "\n" ^
    1.54      mk_eqns eqns ^ "\n(" ^ ss ^ ",\n " ^ mk_list congs ^ ");\n\
    1.55      \in\n\
    1.56      \structure " ^ fid ^ " =\n\
    1.57 @@ -251,7 +251,7 @@
    1.58    in
    1.59      ";\n\n\
    1.60      \local\n\
    1.61 -    \val (thy, result) = thy |> RecdefPackage.defer_recdef " ^ quote fid ^ "\n" ^
    1.62 +    \val (thy, result) = thy |> RecdefPackage.defer_recdef " ^ Library.quote fid ^ "\n" ^
    1.63      axms_text ^ "\n" ^ congs_text ^ ";\n\
    1.64      \in\n\
    1.65      \structure " ^ fid ^ " =\n\
     2.1 --- a/src/Pure/Isar/antiquote.ML	Fri Apr 16 18:44:39 2004 +0200
     2.2 +++ b/src/Pure/Isar/antiquote.ML	Fri Apr 16 18:45:56 2004 +0200
     2.3 @@ -44,7 +44,7 @@
     2.4    | escape "\"" = "\\\""
     2.5    | escape s = s;
     2.6  
     2.7 -val quote_escape = quote o implode o map escape o Symbol.explode;
     2.8 +val quote_escape = Library.quote o implode o map escape o Symbol.explode;
     2.9  
    2.10  val scan_ant =
    2.11    T.scan_blank ||
     3.1 --- a/src/Pure/Isar/isar_thy.ML	Fri Apr 16 18:44:39 2004 +0200
     3.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Apr 16 18:45:56 2004 +0200
     3.3 @@ -565,7 +565,7 @@
     3.4      \val thms = PureThy.get_thms_closure (Context.the_context ());\n\
     3.5      \val method: bstring * (Args.src -> Proof.context -> Proof.method) * string"
     3.6      "PureIsar.Method.add_method method"
     3.7 -    ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")");
     3.8 +    ("(" ^ Library.quote name ^ ", " ^ txt ^ ", " ^ Library.quote cmt ^ ")");
     3.9  
    3.10  
    3.11  (* add_oracle *)
    3.12 @@ -574,7 +574,7 @@
    3.13    Context.use_let
    3.14      "val oracle: bstring * (Sign.sg * Object.T -> term)"
    3.15      "Theory.add_oracle oracle"
    3.16 -    ("(" ^ quote name ^ ", " ^ txt ^ ")");
    3.17 +    ("(" ^ Library.quote name ^ ", " ^ txt ^ ")");
    3.18  
    3.19  
    3.20  (* add_locale *)
     4.1 --- a/src/Pure/Syntax/syntax.ML	Fri Apr 16 18:44:39 2004 +0200
     4.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Apr 16 18:45:56 2004 +0200
     4.3 @@ -264,7 +264,7 @@
     4.4  (** inspect syntax **)
     4.5  
     4.6  fun pretty_strs_qs name strs =
     4.7 -  Pretty.strs (name :: map quote (sort_strings strs));
     4.8 +  Pretty.strs (name :: map Library.quote (sort_strings strs));
     4.9  
    4.10  
    4.11  (* print_gram *)
    4.12 @@ -292,7 +292,7 @@
    4.13      fun pretty_ruletab name tab =
    4.14        Pretty.big_list name (map Ast.pretty_rule (dest_ruletab tab));
    4.15  
    4.16 -    fun pretty_tokentr (mode, trs) = Pretty.strs (quote mode ^ ":" :: map fst trs);
    4.17 +    fun pretty_tokentr (mode, trs) = Pretty.strs (Library.quote mode ^ ":" :: map fst trs);
    4.18  
    4.19      val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab,
    4.20        print_ruletab, print_ast_trtab, tokentrtab, ...} = tabs;
     5.1 --- a/src/Pure/Thy/html.ML	Fri Apr 16 18:44:39 2004 +0200
     5.2 +++ b/src/Pure/Thy/html.ML	Fri Apr 16 18:45:56 2004 +0200
     5.3 @@ -244,7 +244,7 @@
     5.4  (* token translations *)
     5.5  
     5.6  fun style stl =
     5.7 -  apfst (enclose ("<span class=" ^ quote stl ^ ">") "</span>") o output_width;
     5.8 +  apfst (enclose ("<span class=" ^ Library.quote stl ^ ">") "</span>") o output_width;
     5.9  
    5.10  val html_trans =
    5.11   [("class", style "tclass"),
    5.12 @@ -273,7 +273,7 @@
    5.13  
    5.14  (* misc *)
    5.15  
    5.16 -fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>";
    5.17 +fun href_name s txt = "<a href=" ^ Library.quote s ^ ">" ^ txt ^ "</a>";
    5.18  fun href_path path txt = href_name (Url.pack path) txt;
    5.19  
    5.20  fun href_opt_name None txt = txt
     6.1 --- a/src/Pure/Thy/latex.ML	Fri Apr 16 18:44:39 2004 +0200
     6.2 +++ b/src/Pure/Thy/latex.ML	Fri Apr 16 18:45:56 2004 +0200
     6.3 @@ -102,7 +102,7 @@
     6.4            "\\isacommand{" ^ output_syms s ^ "}"
     6.5          else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then
     6.6            "\\isakeyword{" ^ output_syms s ^ "}"
     6.7 -        else if T.is_kind T.String tok then output_syms (quote s)
     6.8 +        else if T.is_kind T.String tok then output_syms (Library.quote s)
     6.9          else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
    6.10          else output_syms s
    6.11        end
     7.1 --- a/src/Pure/Thy/present.ML	Fri Apr 16 18:44:39 2004 +0200
     7.2 +++ b/src/Pure/Thy/present.ML	Fri Apr 16 18:45:56 2004 +0200
     7.3 @@ -100,7 +100,7 @@
     7.4  fun write_graph gr path =
     7.5    File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
     7.6      "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
     7.7 -    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
     7.8 +    path ^ "\" > " ^ space_implode " " (map Library.quote parents) ^ " ;") gr));
     7.9  
    7.10  fun ID_of sess s = space_implode "/" (sess @ [s]);
    7.11  
     8.1 --- a/src/Pure/Thy/thy_parse.ML	Fri Apr 16 18:44:39 2004 +0200
     8.2 +++ b/src/Pure/Thy/thy_parse.ML	Fri Apr 16 18:45:56 2004 +0200
     8.3 @@ -138,7 +138,7 @@
     8.4  val ident = kind Ident;
     8.5  val long_ident = kind LongIdent;
     8.6  val long_id = ident || long_ident;
     8.7 -val type_var = kind TypeVar >> quote;
     8.8 +val type_var = kind TypeVar >> Library.quote;
     8.9  val nat = kind Nat;
    8.10  val string = kind String;
    8.11  val verbatim = kind Verbatim;
    8.12 @@ -181,7 +181,7 @@
    8.13  
    8.14  (* names *)
    8.15  
    8.16 -val name = ident >> quote || string;
    8.17 +val name = ident >> Library.quote || string;
    8.18  val names = list name;
    8.19  val names1 = list1 name;
    8.20  val name_list = names >> mk_list;
    8.21 @@ -202,7 +202,7 @@
    8.22  
    8.23  (* arities *)
    8.24  
    8.25 -val sort = name || "{" $$-- list ident --$$ "}" >> (quote o enclose "{" "}" o commas);
    8.26 +val sort = name || "{" $$-- list ident --$$ "}" >> (Library.quote o enclose "{" "}" o commas);
    8.27  val sort_list1 = list1 sort >> mk_list;
    8.28  
    8.29  val arity = optional ("(" $$-- !! (sort_list1 --$$")")) "[]" -- sort;
    8.30 @@ -273,7 +273,7 @@
    8.31        "(" $$-- const_type true --$$ ")" >> parens) toks
    8.32    end;
    8.33  
    8.34 -val typ = string || (const_type false >> quote);
    8.35 +val typ = string || (const_type false >> Library.quote);
    8.36  
    8.37  
    8.38  fun mk_old_type_decl ((ts, n), syn) =
    8.39 @@ -352,8 +352,8 @@
    8.40  
    8.41  (* axioms *)
    8.42  
    8.43 -val mk_axms = mk_big_list o map (mk_pair o apfst quote);
    8.44 -val mk_axms' = mk_big_list o map (mk_pair o rpair "[]" o mk_pair o apfst quote);
    8.45 +val mk_axms = mk_big_list o map (mk_pair o apfst Library.quote);
    8.46 +val mk_axms' = mk_big_list o map (mk_pair o rpair "[]" o mk_pair o apfst Library.quote);
    8.47  
    8.48  fun mk_axiom_decls axms = (mk_axms axms, map fst axms);
    8.49  
    8.50 @@ -371,7 +371,7 @@
    8.51    let
    8.52      val (axms_defs, axms_names) =
    8.53        mk_axiom_decls (map (fn ((id, _), def) => (id ^ "_def", def)) x);
    8.54 -  in ((mk_big_list o map mk_triple2 o map (apfst quote o fst)) x ^
    8.55 +  in ((mk_big_list o map mk_triple2 o map (apfst Library.quote o fst)) x ^
    8.56         "\n\n|> (#1 oo (PureThy.add_defs false o map Thm.no_attributes))\n" ^ axms_defs, axms_names)
    8.57    end;
    8.58  
    8.59 @@ -416,16 +416,16 @@
    8.60  
    8.61  val locale_decl =
    8.62    (name --$$ "=") -- 
    8.63 -    (optional ((ident >> (fn x => parens ("Some" ^ quote x))) --$$ "+") ("None")) --
    8.64 +    (optional ((ident >> (fn x => parens ("Some" ^ Library.quote x))) --$$ "+") ("None")) --
    8.65      ("fixes" $$--
    8.66        (repeat (name --$$ "::" -- !! (typ -- opt_mixfix)) 
    8.67         >> (mk_big_list o map mk_triple2))) --
    8.68      (optional 
    8.69 -     ("assumes" $$-- (repeat ((ident >> quote) -- !! string) 
    8.70 +     ("assumes" $$-- (repeat ((ident >> Library.quote) -- !! string) 
    8.71  		     >> (mk_list o map mk_pair)))
    8.72       "[]") --
    8.73      (optional 
    8.74 -     ("defines" $$-- (repeat ((ident >> quote) -- !! string) 
    8.75 +     ("defines" $$-- (repeat ((ident >> Library.quote) -- !! string) 
    8.76  		      >> (mk_list o map mk_pair)))
    8.77       "[]")
    8.78    >> (fn ((((nm, ext), cs), asms), defs) => cat_lines [nm, ext, cs, asms, defs]);
    8.79 @@ -454,7 +454,7 @@
    8.80  (* header *)
    8.81  
    8.82  fun mk_header (thy_name, parents) =
    8.83 -  (thy_name, "IsarThy.begin_theory " ^ cat (quote thy_name) (mk_list parents) ^ " []");
    8.84 +  (thy_name, "IsarThy.begin_theory " ^ cat (Library.quote thy_name) (mk_list parents) ^ " []");
    8.85  
    8.86  val header = ident --$$ "=" -- enum1 "+" name >> mk_header;
    8.87  
    8.88 @@ -524,7 +524,7 @@
    8.89  
    8.90  (* standard sections *)
    8.91  
    8.92 -fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy " ^ quote ax ^ ";";
    8.93 +fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy " ^ Library.quote ax ^ ";";
    8.94  val mk_vals = cat_lines o map mk_val;
    8.95  
    8.96  fun mk_axm_sect "" (txt, axs) = (txt, mk_vals axs)
     9.1 --- a/src/Pure/codegen.ML	Fri Apr 16 18:44:39 2004 +0200
     9.2 +++ b/src/Pure/codegen.ML	Fri Apr 16 18:45:56 2004 +0200
     9.3 @@ -491,7 +491,8 @@
     9.4  fun output_code gr xs = implode (map (snd o Graph.get_node gr)
     9.5    (rev (Graph.all_preds gr xs)));
     9.6  
     9.7 -fun gen_generate_code prep_term thy = Pretty.setmp_margin (!margin) (fn xs =>
     9.8 +fun gen_generate_code prep_term thy =
     9.9 +  setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs =>
    9.10    let
    9.11      val sg = sign_of thy;
    9.12      val gr = Graph.new_node ("<Top>", (None, "")) Graph.empty;
    9.13 @@ -504,7 +505,7 @@
    9.14      space_implode "\n\n" (map (fn (s', p) => Pretty.string_of (Pretty.block
    9.15        [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"])) ps) ^
    9.16      "\n\nend;\n\nopen Generated;\n"
    9.17 -  end);
    9.18 +  end));
    9.19  
    9.20  val generate_code_i = gen_generate_code (K I);
    9.21  val generate_code = gen_generate_code
    9.22 @@ -574,7 +575,7 @@
    9.23                Pretty.block [Pretty.str "Library.Some ", Pretty.block (Pretty.str "[" ::
    9.24                  flat (separate [Pretty.str ",", Pretty.brk 1]
    9.25                    (map (fn (s, T) => [Pretty.block
    9.26 -                    [Pretty.str ("(" ^ quote s ^ ","), Pretty.brk 1,
    9.27 +                    [Pretty.str ("(" ^ Library.quote s ^ ","), Pretty.brk 1,
    9.28                       mk_app false (mk_term_of sg false T)
    9.29                         [Pretty.str s], Pretty.str ")"]]) frees)) @
    9.30                    [Pretty.str "]"])]],
    10.1 --- a/src/Pure/display.ML	Fri Apr 16 18:44:39 2004 +0200
    10.2 +++ b/src/Pure/display.ML	Fri Apr 16 18:45:56 2004 +0200
    10.3 @@ -64,7 +64,7 @@
    10.4  val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
    10.5  val show_tags = ref false;      (*false: suppress tags*)
    10.6  
    10.7 -fun pretty_tag (name, args) = Pretty.strs (name :: map quote args);
    10.8 +fun pretty_tag (name, args) = Pretty.strs (name :: map Library.quote args);
    10.9  val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
   10.10  
   10.11  fun pretty_flexpair pretty_term (t, u) = Pretty.block
   10.12 @@ -166,8 +166,8 @@
   10.13  fun pretty_name_space (kind, space) =
   10.14    let
   10.15      fun prt_entry (name, accs) = Pretty.block
   10.16 -      (Pretty.str (quote name ^ " =") :: Pretty.brk 1 ::
   10.17 -        Pretty.commas (map (Pretty.str o quote) accs));
   10.18 +      (Pretty.str (Library.quote name ^ " =") :: Pretty.brk 1 ::
   10.19 +        Pretty.commas (map (Pretty.quote o Pretty.str) accs));
   10.20    in
   10.21      Pretty.fbreaks (Pretty.str (kind ^ ":") :: map prt_entry (NameSpace.dest space))
   10.22      |> Pretty.block
    11.1 --- a/src/ZF/thy_syntax.ML	Fri Apr 16 18:44:39 2004 +0200
    11.2 +++ b/src/ZF/thy_syntax.ML	Fri Apr 16 18:45:56 2004 +0200
    11.3 @@ -43,7 +43,7 @@
    11.4                             (map (scan_to_id o unenclose) recs)
    11.5            and srec_tms = mk_list recs
    11.6            and sintrs   =
    11.7 -            mk_big_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) ipairs)
    11.8 +            mk_big_list (map (fn (x, y) => mk_pair (mk_pair (Library.quote x, y), "[]")) ipairs)
    11.9            and inames   = mk_list (map (mk_bind "" o fst) ipairs)
   11.10        in
   11.11           ";\n\n\
   11.12 @@ -155,7 +155,7 @@
   11.13  fun mk_primrec_decl eqns =
   11.14    let val binds = map (mk_bind "" o fst) eqns in
   11.15      ";\nval (thy, " ^ mk_list binds ^ ") = PrimrecPackage.add_primrec " ^
   11.16 -      mk_list (map (fn p => mk_pair (mk_pair p, "[]")) (map (apfst quote) eqns)) ^ " " ^ " thy;\n\
   11.17 +      mk_list (map (fn p => mk_pair (mk_pair p, "[]")) (map (apfst Library.quote) eqns)) ^ " " ^ " thy;\n\
   11.18      \val thy = thy\n"
   11.19    end;
   11.20