# 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;