# HG changeset patch # User berghofe # Date 1082133956 -7200 # Node ID 7009f59711e367c6fd04b3748d10fb1982fdf77b # Parent ee0fb03f5f1e327e8566b22e124c5d94fd1d4a4b Replaced quote by Library.quote, since quote now refers to Symbol.quote diff -r ee0fb03f5f1e -r 7009f59711e3 src/HOL/thy_syntax.ML --- a/src/HOL/thy_syntax.ML Fri Apr 16 18:44:39 2004 +0200 +++ b/src/HOL/thy_syntax.ML Fri Apr 16 18:45:56 2004 +0200 @@ -57,7 +57,7 @@ fun mk_params ((recs, ipairs), monos) = let val big_rec_name = space_implode "_" (map (scan_to_id o unenclose) recs) and srec_tms = mk_list recs - and sintrs = mk_big_list (no_atts (map (mk_pair o apfst quote) ipairs)) + and sintrs = mk_big_list (no_atts (map (mk_pair o apfst Library.quote) ipairs)) in ";\n\n\ \local\n\ @@ -133,7 +133,7 @@ val names = map (fn ((((alt_name, _), name), _), _) => unenclose (if_none alt_name name)) dts; - val add_datatype_args = brackets (commas (map quote names)) ^ " " ^ + val add_datatype_args = brackets (commas (map Library.quote names)) ^ " " ^ brackets (commas (map (fn ((((_, vs), name), mx), cs) => parens (brackets (commas vs) ^ ", " ^ name ^ ", " ^ mx ^ ", " ^ brackets (commas cs))) dts)); @@ -156,7 +156,7 @@ \ case_thms, split_thms, induction, size, simps}) =\n\ \ DatatypePackage.rep_datatype " ^ (case names of - Some names => "(Some [" ^ commas_quote names ^ "])\n " ^ + Some names => "(Some [" ^ Library.commas_quote names ^ "])\n " ^ mk_thmss distinct ^ "\n " ^ mk_thmss inject ^ "\n " ^ mk_thm induct ^ " thy;\nin\n" ^ mk_bind_thms_string names | None => "None\n " ^ mk_thmss distinct ^ "\n " ^ mk_thmss inject ^ @@ -179,7 +179,7 @@ val opt_typs = repeat ((string >> unenclose) || simple_typ || ("(" $$-- complex_typ --$$ ")")); val constructor = name -- opt_typs -- opt_mixfix >> (fn ((n, Ts), mx) => - parens (n ^ ", " ^ brackets (commas_quote Ts) ^ ", " ^ mx)); + parens (n ^ ", " ^ brackets (Library.commas_quote Ts) ^ ", " ^ mx)); val opt_name = optional ("(" $$-- name --$$ ")" >> Some) None fun optlistlist s = optional (s $$-- enum "and" (list name)) [[]] @@ -199,7 +199,7 @@ (** primrec **) fun mk_patterns eqns = mk_list (map (fn (s, _) => if s = "" then "_" else s) eqns); -fun mk_eqns eqns = mk_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) eqns); +fun mk_eqns eqns = mk_list (map (fn (x, y) => mk_pair (mk_pair (Library.quote x, y), "[]")) eqns); fun mk_primrec_decl (alt_name, eqns) = ";\nval (thy, " ^ mk_patterns eqns ^ ") = PrimrecPackage.add_primrec " ^ alt_name ^ " " @@ -221,7 +221,7 @@ ";\n\n\ \local\n\ \fun simpset() = Simplifier.simpset_of thy;\n\ - \val (thy, result) = thy |> RecdefPackage.add_recdef_old " ^ quote fid ^ " " ^ rel ^ "\n" ^ + \val (thy, result) = thy |> RecdefPackage.add_recdef_old " ^ Library.quote fid ^ " " ^ rel ^ "\n" ^ mk_eqns eqns ^ "\n(" ^ ss ^ ",\n " ^ mk_list congs ^ ");\n\ \in\n\ \structure " ^ fid ^ " =\n\ @@ -251,7 +251,7 @@ in ";\n\n\ \local\n\ - \val (thy, result) = thy |> RecdefPackage.defer_recdef " ^ quote fid ^ "\n" ^ + \val (thy, result) = thy |> RecdefPackage.defer_recdef " ^ Library.quote fid ^ "\n" ^ axms_text ^ "\n" ^ congs_text ^ ";\n\ \in\n\ \structure " ^ fid ^ " =\n\ diff -r ee0fb03f5f1e -r 7009f59711e3 src/Pure/Isar/antiquote.ML --- a/src/Pure/Isar/antiquote.ML Fri Apr 16 18:44:39 2004 +0200 +++ b/src/Pure/Isar/antiquote.ML Fri Apr 16 18:45:56 2004 +0200 @@ -44,7 +44,7 @@ | escape "\"" = "\\\"" | escape s = s; -val quote_escape = quote o implode o map escape o Symbol.explode; +val quote_escape = Library.quote o implode o map escape o Symbol.explode; val scan_ant = T.scan_blank || diff -r ee0fb03f5f1e -r 7009f59711e3 src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Fri Apr 16 18:44:39 2004 +0200 +++ b/src/Pure/Isar/isar_thy.ML Fri Apr 16 18:45:56 2004 +0200 @@ -565,7 +565,7 @@ \val thms = PureThy.get_thms_closure (Context.the_context ());\n\ \val method: bstring * (Args.src -> Proof.context -> Proof.method) * string" "PureIsar.Method.add_method method" - ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")"); + ("(" ^ Library.quote name ^ ", " ^ txt ^ ", " ^ Library.quote cmt ^ ")"); (* add_oracle *) @@ -574,7 +574,7 @@ Context.use_let "val oracle: bstring * (Sign.sg * Object.T -> term)" "Theory.add_oracle oracle" - ("(" ^ quote name ^ ", " ^ txt ^ ")"); + ("(" ^ Library.quote name ^ ", " ^ txt ^ ")"); (* add_locale *) diff -r ee0fb03f5f1e -r 7009f59711e3 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Fri Apr 16 18:44:39 2004 +0200 +++ b/src/Pure/Syntax/syntax.ML Fri Apr 16 18:45:56 2004 +0200 @@ -264,7 +264,7 @@ (** inspect syntax **) fun pretty_strs_qs name strs = - Pretty.strs (name :: map quote (sort_strings strs)); + Pretty.strs (name :: map Library.quote (sort_strings strs)); (* print_gram *) @@ -292,7 +292,7 @@ fun pretty_ruletab name tab = Pretty.big_list name (map Ast.pretty_rule (dest_ruletab tab)); - fun pretty_tokentr (mode, trs) = Pretty.strs (quote mode ^ ":" :: map fst trs); + fun pretty_tokentr (mode, trs) = Pretty.strs (Library.quote mode ^ ":" :: map fst trs); val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab, print_ast_trtab, tokentrtab, ...} = tabs; diff -r ee0fb03f5f1e -r 7009f59711e3 src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Fri Apr 16 18:44:39 2004 +0200 +++ b/src/Pure/Thy/html.ML Fri Apr 16 18:45:56 2004 +0200 @@ -244,7 +244,7 @@ (* token translations *) fun style stl = - apfst (enclose ("") "") o output_width; + apfst (enclose ("") "") o output_width; val html_trans = [("class", style "tclass"), @@ -273,7 +273,7 @@ (* misc *) -fun href_name s txt = "" ^ txt ^ ""; +fun href_name s txt = "" ^ txt ^ ""; fun href_path path txt = href_name (Url.pack path) txt; fun href_opt_name None txt = txt diff -r ee0fb03f5f1e -r 7009f59711e3 src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Fri Apr 16 18:44:39 2004 +0200 +++ b/src/Pure/Thy/latex.ML Fri Apr 16 18:45:56 2004 +0200 @@ -102,7 +102,7 @@ "\\isacommand{" ^ output_syms s ^ "}" else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then "\\isakeyword{" ^ output_syms s ^ "}" - else if T.is_kind T.String tok then output_syms (quote s) + else if T.is_kind T.String tok then output_syms (Library.quote s) else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s) else output_syms s end diff -r ee0fb03f5f1e -r 7009f59711e3 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Fri Apr 16 18:44:39 2004 +0200 +++ b/src/Pure/Thy/present.ML Fri Apr 16 18:45:56 2004 +0200 @@ -100,7 +100,7 @@ fun write_graph gr path = File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} => "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^ - path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr)); + path ^ "\" > " ^ space_implode " " (map Library.quote parents) ^ " ;") gr)); fun ID_of sess s = space_implode "/" (sess @ [s]); diff -r ee0fb03f5f1e -r 7009f59711e3 src/Pure/Thy/thy_parse.ML --- a/src/Pure/Thy/thy_parse.ML Fri Apr 16 18:44:39 2004 +0200 +++ b/src/Pure/Thy/thy_parse.ML Fri Apr 16 18:45:56 2004 +0200 @@ -138,7 +138,7 @@ val ident = kind Ident; val long_ident = kind LongIdent; val long_id = ident || long_ident; -val type_var = kind TypeVar >> quote; +val type_var = kind TypeVar >> Library.quote; val nat = kind Nat; val string = kind String; val verbatim = kind Verbatim; @@ -181,7 +181,7 @@ (* names *) -val name = ident >> quote || string; +val name = ident >> Library.quote || string; val names = list name; val names1 = list1 name; val name_list = names >> mk_list; @@ -202,7 +202,7 @@ (* arities *) -val sort = name || "{" $$-- list ident --$$ "}" >> (quote o enclose "{" "}" o commas); +val sort = name || "{" $$-- list ident --$$ "}" >> (Library.quote o enclose "{" "}" o commas); val sort_list1 = list1 sort >> mk_list; val arity = optional ("(" $$-- !! (sort_list1 --$$")")) "[]" -- sort; @@ -273,7 +273,7 @@ "(" $$-- const_type true --$$ ")" >> parens) toks end; -val typ = string || (const_type false >> quote); +val typ = string || (const_type false >> Library.quote); fun mk_old_type_decl ((ts, n), syn) = @@ -352,8 +352,8 @@ (* axioms *) -val mk_axms = mk_big_list o map (mk_pair o apfst quote); -val mk_axms' = mk_big_list o map (mk_pair o rpair "[]" o mk_pair o apfst quote); +val mk_axms = mk_big_list o map (mk_pair o apfst Library.quote); +val mk_axms' = mk_big_list o map (mk_pair o rpair "[]" o mk_pair o apfst Library.quote); fun mk_axiom_decls axms = (mk_axms axms, map fst axms); @@ -371,7 +371,7 @@ let val (axms_defs, axms_names) = mk_axiom_decls (map (fn ((id, _), def) => (id ^ "_def", def)) x); - in ((mk_big_list o map mk_triple2 o map (apfst quote o fst)) x ^ + in ((mk_big_list o map mk_triple2 o map (apfst Library.quote o fst)) x ^ "\n\n|> (#1 oo (PureThy.add_defs false o map Thm.no_attributes))\n" ^ axms_defs, axms_names) end; @@ -416,16 +416,16 @@ val locale_decl = (name --$$ "=") -- - (optional ((ident >> (fn x => parens ("Some" ^ quote x))) --$$ "+") ("None")) -- + (optional ((ident >> (fn x => parens ("Some" ^ Library.quote x))) --$$ "+") ("None")) -- ("fixes" $$-- (repeat (name --$$ "::" -- !! (typ -- opt_mixfix)) >> (mk_big_list o map mk_triple2))) -- (optional - ("assumes" $$-- (repeat ((ident >> quote) -- !! string) + ("assumes" $$-- (repeat ((ident >> Library.quote) -- !! string) >> (mk_list o map mk_pair))) "[]") -- (optional - ("defines" $$-- (repeat ((ident >> quote) -- !! string) + ("defines" $$-- (repeat ((ident >> Library.quote) -- !! string) >> (mk_list o map mk_pair))) "[]") >> (fn ((((nm, ext), cs), asms), defs) => cat_lines [nm, ext, cs, asms, defs]); @@ -454,7 +454,7 @@ (* header *) fun mk_header (thy_name, parents) = - (thy_name, "IsarThy.begin_theory " ^ cat (quote thy_name) (mk_list parents) ^ " []"); + (thy_name, "IsarThy.begin_theory " ^ cat (Library.quote thy_name) (mk_list parents) ^ " []"); val header = ident --$$ "=" -- enum1 "+" name >> mk_header; @@ -524,7 +524,7 @@ (* standard sections *) -fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy " ^ quote ax ^ ";"; +fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy " ^ Library.quote ax ^ ";"; val mk_vals = cat_lines o map mk_val; fun mk_axm_sect "" (txt, axs) = (txt, mk_vals axs) diff -r ee0fb03f5f1e -r 7009f59711e3 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Fri Apr 16 18:44:39 2004 +0200 +++ b/src/Pure/codegen.ML Fri Apr 16 18:45:56 2004 +0200 @@ -491,7 +491,8 @@ fun output_code gr xs = implode (map (snd o Graph.get_node gr) (rev (Graph.all_preds gr xs))); -fun gen_generate_code prep_term thy = Pretty.setmp_margin (!margin) (fn xs => +fun gen_generate_code prep_term thy = + setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs => let val sg = sign_of thy; val gr = Graph.new_node ("", (None, "")) Graph.empty; @@ -504,7 +505,7 @@ space_implode "\n\n" (map (fn (s', p) => Pretty.string_of (Pretty.block [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"])) ps) ^ "\n\nend;\n\nopen Generated;\n" - end); + end)); val generate_code_i = gen_generate_code (K I); val generate_code = gen_generate_code @@ -574,7 +575,7 @@ Pretty.block [Pretty.str "Library.Some ", Pretty.block (Pretty.str "[" :: flat (separate [Pretty.str ",", Pretty.brk 1] (map (fn (s, T) => [Pretty.block - [Pretty.str ("(" ^ quote s ^ ","), Pretty.brk 1, + [Pretty.str ("(" ^ Library.quote s ^ ","), Pretty.brk 1, mk_app false (mk_term_of sg false T) [Pretty.str s], Pretty.str ")"]]) frees)) @ [Pretty.str "]"])]], diff -r ee0fb03f5f1e -r 7009f59711e3 src/Pure/display.ML --- a/src/Pure/display.ML Fri Apr 16 18:44:39 2004 +0200 +++ b/src/Pure/display.ML Fri Apr 16 18:45:56 2004 +0200 @@ -64,7 +64,7 @@ val show_hyps = ref false; (*false: print meta-hypotheses as dots*) val show_tags = ref false; (*false: suppress tags*) -fun pretty_tag (name, args) = Pretty.strs (name :: map quote args); +fun pretty_tag (name, args) = Pretty.strs (name :: map Library.quote args); val pretty_tags = Pretty.list "[" "]" o map pretty_tag; fun pretty_flexpair pretty_term (t, u) = Pretty.block @@ -166,8 +166,8 @@ fun pretty_name_space (kind, space) = let fun prt_entry (name, accs) = Pretty.block - (Pretty.str (quote name ^ " =") :: Pretty.brk 1 :: - Pretty.commas (map (Pretty.str o quote) accs)); + (Pretty.str (Library.quote name ^ " =") :: Pretty.brk 1 :: + Pretty.commas (map (Pretty.quote o Pretty.str) accs)); in Pretty.fbreaks (Pretty.str (kind ^ ":") :: map prt_entry (NameSpace.dest space)) |> Pretty.block diff -r ee0fb03f5f1e -r 7009f59711e3 src/ZF/thy_syntax.ML --- a/src/ZF/thy_syntax.ML Fri Apr 16 18:44:39 2004 +0200 +++ b/src/ZF/thy_syntax.ML Fri Apr 16 18:45:56 2004 +0200 @@ -43,7 +43,7 @@ (map (scan_to_id o unenclose) recs) and srec_tms = mk_list recs and sintrs = - mk_big_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) ipairs) + mk_big_list (map (fn (x, y) => mk_pair (mk_pair (Library.quote x, y), "[]")) ipairs) and inames = mk_list (map (mk_bind "" o fst) ipairs) in ";\n\n\ @@ -155,7 +155,7 @@ fun mk_primrec_decl eqns = let val binds = map (mk_bind "" o fst) eqns in ";\nval (thy, " ^ mk_list binds ^ ") = PrimrecPackage.add_primrec " ^ - mk_list (map (fn p => mk_pair (mk_pair p, "[]")) (map (apfst quote) eqns)) ^ " " ^ " thy;\n\ + mk_list (map (fn p => mk_pair (mk_pair p, "[]")) (map (apfst Library.quote) eqns)) ^ " " ^ " thy;\n\ \val thy = thy\n" end;