--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Sat May 08 20:01:28 2010 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Sat May 08 20:14:11 2010 +0200
@@ -212,8 +212,7 @@
text {*
\begin{mldecls}
- @{index_ML Pretty.setdepth: "int -> unit"} \\
- @{index_ML Pretty.setmargin: "int -> unit"} \\
+ @{index_ML Pretty.margin_default: "int Unsynchronized.ref"} \\
@{index_ML print_depth: "int -> unit"} \\
\end{mldecls}
@@ -221,16 +220,12 @@
\begin{description}
- \item @{ML Pretty.setdepth}~@{text d} tells the pretty printer to
- limit the printing depth to @{text d}. This affects the display of
- types, terms, theorems etc. The default value is 0, which permits
- printing to an arbitrary depth. Other useful values for @{text d}
- are 10 and 20.
-
- \item @{ML Pretty.setmargin}~@{text m} tells the pretty printer to
- assume a right margin (page width) of @{text m}. The initial margin
- is 76, but user interfaces might adapt the margin automatically when
- resizing windows.
+ \item @{ML Pretty.margin_default} indicates the global default for
+ the right margin of the built-in pretty printer, with initial value
+ 76. Note that user-interfaces typically control margins
+ automatically when resizing windows, or even bypass the formatting
+ engine of Isabelle/ML altogether and do it within the front end via
+ Isabelle/Scala.
\item @{ML print_depth}~@{text n} limits the printing depth of the
ML toplevel pretty printer; the precise effect depends on the ML
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat May 08 20:01:28 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat May 08 20:14:11 2010 +0200
@@ -231,8 +231,7 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML}{Pretty.setdepth}\verb|Pretty.setdepth: int -> unit| \\
- \indexdef{}{ML}{Pretty.setmargin}\verb|Pretty.setmargin: int -> unit| \\
+ \indexdef{}{ML}{Pretty.margin\_default}\verb|Pretty.margin_default: int Unsynchronized.ref| \\
\indexdef{}{ML}{print\_depth}\verb|print_depth: int -> unit| \\
\end{mldecls}
@@ -240,16 +239,12 @@
\begin{description}
- \item \verb|Pretty.setdepth|~\isa{d} tells the pretty printer to
- limit the printing depth to \isa{d}. This affects the display of
- types, terms, theorems etc. The default value is 0, which permits
- printing to an arbitrary depth. Other useful values for \isa{d}
- are 10 and 20.
-
- \item \verb|Pretty.setmargin|~\isa{m} tells the pretty printer to
- assume a right margin (page width) of \isa{m}. The initial margin
- is 76, but user interfaces might adapt the margin automatically when
- resizing windows.
+ \item \verb|Pretty.margin_default| indicates the global default for
+ the right margin of the built-in pretty printer, with initial value
+ 76. Note that user-interfaces typically control margins
+ automatically when resizing windows, or even bypass the formatting
+ engine of Isabelle/ML altogether and do it within the front end via
+ Isabelle/Scala.
\item \verb|print_depth|~\isa{n} limits the printing depth of the
ML toplevel pretty printer; the precise effect depends on the ML
--- a/doc-src/TutorialI/Rules/Primes.thy Sat May 08 20:01:28 2010 +0200
+++ b/doc-src/TutorialI/Rules/Primes.thy Sat May 08 20:14:11 2010 +0200
@@ -9,7 +9,7 @@
"gcd m n = (if n=0 then m else gcd n (m mod n))"
-ML "Pretty.setmargin 64"
+ML "Pretty.margin_default := 64"
ML "ThyOutput.indent := 5" (*that is, Doc/TutorialI/settings.ML*)
--- a/doc-src/TutorialI/Sets/Examples.thy Sat May 08 20:01:28 2010 +0200
+++ b/doc-src/TutorialI/Sets/Examples.thy Sat May 08 20:14:11 2010 +0200
@@ -2,7 +2,7 @@
theory Examples imports Main Binomial begin
ML "Unsynchronized.reset eta_contract"
-ML "Pretty.setmargin 64"
+ML "Pretty.margin_default := 64"
text{*membership, intersection *}
text{*difference and empty set*}
--- a/doc-src/TutorialI/Sets/Functions.thy Sat May 08 20:01:28 2010 +0200
+++ b/doc-src/TutorialI/Sets/Functions.thy Sat May 08 20:14:11 2010 +0200
@@ -1,7 +1,7 @@
(* ID: $Id$ *)
theory Functions imports Main begin
-ML "Pretty.setmargin 64"
+ML "Pretty.margin_default := 64"
text{*
--- a/doc-src/TutorialI/Sets/Recur.thy Sat May 08 20:01:28 2010 +0200
+++ b/doc-src/TutorialI/Sets/Recur.thy Sat May 08 20:14:11 2010 +0200
@@ -1,7 +1,7 @@
(* ID: $Id$ *)
theory Recur imports Main begin
-ML "Pretty.setmargin 64"
+ML "Pretty.margin_default := 64"
text{*
--- a/doc-src/TutorialI/Sets/Relations.thy Sat May 08 20:01:28 2010 +0200
+++ b/doc-src/TutorialI/Sets/Relations.thy Sat May 08 20:14:11 2010 +0200
@@ -1,7 +1,7 @@
(* ID: $Id$ *)
theory Relations imports Main begin
-ML "Pretty.setmargin 64"
+ML "Pretty.margin_default := 64"
(*Id is only used in UNITY*)
(*refl, antisym,trans,univalent,\<dots> ho hum*)
--- a/doc-src/TutorialI/Types/Numbers.thy Sat May 08 20:01:28 2010 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy Sat May 08 20:14:11 2010 +0200
@@ -2,7 +2,7 @@
imports Complex_Main
begin
-ML "Pretty.setmargin 64"
+ML "Pretty.margin_default := 64"
ML "ThyOutput.indent := 0" (*we don't want 5 for listing theorems*)
text{*
--- a/doc-src/TutorialI/Types/document/Numbers.tex Sat May 08 20:01:28 2010 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Sat May 08 20:14:11 2010 +0200
@@ -26,7 +26,7 @@
%
\isatagML
\isacommand{ML}\isamarkupfalse%
-\ {\isachardoublequoteopen}Pretty{\isachardot}setmargin\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}Pretty{\isachardot}margin{\isacharunderscore}default\ {\isacharcolon}{\isacharequal}\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}\isanewline
\isacommand{ML}\isamarkupfalse%
\ {\isachardoublequoteopen}ThyOutput{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%
\endisatagML
--- a/doc-src/more_antiquote.ML Sat May 08 20:01:28 2010 +0200
+++ b/doc-src/more_antiquote.ML Sat May 08 20:14:11 2010 +0200
@@ -51,7 +51,7 @@
local
-val pr_text = enclose "\\isa{" "}" o Pretty.output o Pretty.str;
+val pr_text = enclose "\\isa{" "}" o Pretty.output NONE o Pretty.str;
fun pr_class ctxt = ProofContext.read_class ctxt
#> Type.extern_class (ProofContext.tsig_of ctxt)
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Sat May 08 20:14:11 2010 +0200
@@ -13,7 +13,7 @@
fun run id ({pre, post, timeout, log, ...}: Mirabelle.run_args) =
let
val thms = Mirabelle.theorems_of_sucessful_proof post
- val names = map Thm.get_name thms
+ val names = map Thm.get_name_hint thms
val add_info = if null names then I else suffix (":\n" ^ commas names)
val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
--- a/src/HOL/Mutabelle/mutabelle.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML Sat May 08 20:14:11 2010 +0200
@@ -648,7 +648,7 @@
val mutated = mutate option (prop_of x) usedthy
commutatives forbidden_funs iter
val (passednum,_,cenum,_) = qc_test mutated insts usedthy sz qciter
- val thmname = "\ntheorem " ^ (Thm.get_name x) ^ ":"
+ val thmname = "\ntheorem " ^ Thm.get_name_hint x ^ ":"
val pnumstring = string_of_int passednum
val cenumstring = string_of_int cenum
in
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sat May 08 20:14:11 2010 +0200
@@ -302,7 +302,7 @@
end
fun create_entry thy thm exec mutants mtds =
- (Thm.get_name thm, exec, map (test_mutants_using_one_method thy mutants) mtds)
+ (Thm.get_name_hint thm, exec, map (test_mutants_using_one_method thy mutants) mtds)
*)
fun create_detailed_entry thy thm exec mutants mtds =
let
@@ -310,7 +310,7 @@
map (fn (mtd_name, invoke_mtd) =>
(mtd_name, safe_invoke_mtd thy (mtd_name, invoke_mtd) mutant)) mtds)
in
- (Thm.get_name thm, exec, prop_of thm, map create_mutant_subentry mutants)
+ (Thm.get_name_hint thm, exec, prop_of thm, map create_mutant_subentry mutants)
end
(* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *)
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Sat May 08 20:14:11 2010 +0200
@@ -120,7 +120,7 @@
REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
REPEAT (etac allE i) THEN atac i)) 1)]);
- val ind_name = Thm.get_name induct;
+ val ind_name = Thm.derivation_name induct;
val vs = map (fn i => List.nth (pnames, i)) is;
val (thm', thy') = thy
|> Sign.root_path
@@ -191,7 +191,7 @@
[asm_simp_tac (HOL_basic_ss addsimps case_rewrites),
resolve_tac prems, asm_simp_tac HOL_basic_ss])]);
- val exh_name = Thm.get_name exhaust;
+ val exh_name = Thm.derivation_name exhaust;
val (thm', thy') = thy
|> Sign.root_path
|> PureThy.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
--- a/src/HOL/Tools/inductive_realizer.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Sat May 08 20:14:11 2010 +0200
@@ -408,7 +408,7 @@
in
Extraction.add_realizers_i
(map (fn (((ind, corr), rlz), r) =>
- mk_realizer thy' (vs' @ Ps) (Thm.get_name ind, ind, corr, rlz, r))
+ mk_realizer thy' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
realizers @ (case realizers of
[(((ind, corr), rlz), r)] =>
[mk_realizer thy' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
--- a/src/Pure/General/pretty.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/General/pretty.ML Sat May 08 20:14:11 2010 +0200
@@ -52,17 +52,16 @@
val big_list: string -> T list -> T
val indent: int -> T -> T
val unbreakable: T -> T
- val setmargin: int -> unit
- val setmp_margin_CRITICAL: int -> ('a -> 'b) -> 'a -> 'b
- val setdepth: int -> unit
- val to_ML: T -> ML_Pretty.pretty
- val from_ML: ML_Pretty.pretty -> T
+ val margin_default: int Unsynchronized.ref
val symbolicN: string
- val output_buffer: T -> Buffer.T
- val output: T -> output
+ val output_buffer: int option -> T -> Buffer.T
+ val output: int option -> T -> output
+ val string_of_margin: int -> T -> string
val string_of: T -> string
val str_of: T -> string
val writeln: T -> unit
+ val to_ML: T -> ML_Pretty.pretty
+ val from_ML: ML_Pretty.pretty -> T
type pp
val pp: (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T) -> pp
val term: pp -> term -> T
@@ -179,34 +178,6 @@
(** formatting **)
-(* margin *)
-
-fun make_margin_info m =
- {margin = m, (*right margin, or page width*)
- breakgain = m div 20, (*minimum added space required of a break*)
- emergencypos = m div 2}; (*position too far to right*)
-
-val margin_info = Unsynchronized.ref (make_margin_info 76);
-fun setmargin m = margin_info := make_margin_info m;
-fun setmp_margin_CRITICAL m f = setmp_CRITICAL margin_info (make_margin_info m) f;
-
-
-(* depth limitation *)
-
-val depth = Unsynchronized.ref 0; (*maximum depth; 0 means no limit*)
-fun setdepth dp = (depth := dp);
-
-local
- fun pruning dp (Block (m, bes, indent, _)) =
- if dp > 0
- then block_markup m (indent, map (pruning (dp - 1)) bes)
- else str "..."
- | pruning _ e = e;
-in
- fun prune e = if ! depth > 0 then pruning (! depth) e else e;
-end;
-
-
(* formatted output *)
local
@@ -259,42 +230,45 @@
| forcenext (Break _ :: es) = fbrk :: es
| forcenext (e :: es) = e :: forcenext es;
-(*es is list of expressions to print;
- blockin is the indentation of the current block;
- after is the width of the following context until next break.*)
-fun format ([], _, _) text = text
- | format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
- (case e of
- Block ((bg, en), bes, indent, _) =>
- let
- val {emergencypos, ...} = ! margin_info;
- val pos' = pos + indent;
- val pos'' = pos' mod emergencypos;
- val block' =
- if pos' < emergencypos then (ind |> add_indent indent, pos')
- else (add_indent pos'' Buffer.empty, pos'');
- val btext: text = text
- |> control bg
- |> format (bes, block', breakdist (es, after))
- |> control en;
- (*if this block was broken then force the next break*)
- val es' = if nl < #nl btext then forcenext es else es;
- in format (es', block, after) btext end
- | Break (force, wd) =>
- let val {margin, breakgain, ...} = ! margin_info in
- (*no break if text to next break fits on this line
- or if breaking would add only breakgain to space*)
- format (es, block, after)
- (if not force andalso
- pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
- then text |> blanks wd (*just insert wd blanks*)
- else text |> newline |> indentation block)
- end
- | String str => format (es, block, after) (string str text));
-
in
-fun formatted e = #tx (format ([prune e], (Buffer.empty, 0), 0) empty);
+fun formatted margin input =
+ let
+ val breakgain = margin div 20; (*minimum added space required of a break*)
+ val emergencypos = margin div 2; (*position too far to right*)
+
+ (*es is list of expressions to print;
+ blockin is the indentation of the current block;
+ after is the width of the following context until next break.*)
+ fun format ([], _, _) text = text
+ | format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
+ (case e of
+ Block ((bg, en), bes, indent, _) =>
+ let
+ val pos' = pos + indent;
+ val pos'' = pos' mod emergencypos;
+ val block' =
+ if pos' < emergencypos then (ind |> add_indent indent, pos')
+ else (add_indent pos'' Buffer.empty, pos'');
+ val btext: text = text
+ |> control bg
+ |> format (bes, block', breakdist (es, after))
+ |> control en;
+ (*if this block was broken then force the next break*)
+ val es' = if nl < #nl btext then forcenext es else es;
+ in format (es', block, after) btext end
+ | Break (force, wd) =>
+ (*no break if text to next break fits on this line
+ or if breaking would add only breakgain to space*)
+ format (es, block, after)
+ (if not force andalso
+ pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
+ then text |> blanks wd (*just insert wd blanks*)
+ else text |> newline |> indentation block)
+ | String str => format (es, block, after) (string str text));
+ in
+ #tx (format ([input], (Buffer.empty, 0), 0) empty)
+ end;
end;
@@ -318,10 +292,28 @@
fun fmt (Block ((bg, en), prts, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
| fmt (String (s, _)) = Buffer.add s
| fmt (Break (_, wd)) = Buffer.add (output_spaces wd);
- in fmt (prune prt) Buffer.empty end;
+ in fmt prt Buffer.empty end;
-(* ML toplevel pretty printing *)
+(* output interfaces *)
+
+val margin_default = Unsynchronized.ref 76; (*right margin, or page width*)
+
+val symbolicN = "pretty_symbolic";
+
+fun output_buffer margin prt =
+ if print_mode_active symbolicN then symbolic prt
+ else formatted (the_default (! margin_default) margin) prt;
+
+val output = Buffer.content oo output_buffer;
+fun string_of_margin margin = Output.escape o output (SOME margin);
+val string_of = Output.escape o output NONE;
+val str_of = Output.escape o Buffer.content o unformatted;
+val writeln = Output.writeln o string_of;
+
+
+
+(** ML toplevel pretty printing **)
fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (m, map to_ML prts, ind)
| to_ML (String s) = ML_Pretty.String s
@@ -332,20 +324,6 @@
| from_ML (ML_Pretty.Break b) = Break b;
-(* output interfaces *)
-
-val symbolicN = "pretty_symbolic";
-
-fun output_buffer prt =
- if print_mode_active symbolicN then symbolic prt
- else formatted prt;
-
-val output = Buffer.content o output_buffer;
-val string_of = Output.escape o output;
-val str_of = Output.escape o Buffer.content o unformatted;
-val writeln = Output.writeln o string_of;
-
-
(** abstract pretty printing context **)
--- a/src/Pure/General/pretty.scala Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/General/pretty.scala Sat May 08 20:14:11 2010 +0200
@@ -78,9 +78,9 @@
Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
}
- private val default_margin = 76
+ private val margin_default = 76
- def formatted(input: List[XML.Tree], margin: Int = default_margin): List[XML.Tree] =
+ def formatted(input: List[XML.Tree], margin: Int = margin_default): List[XML.Tree] =
{
val breakgain = margin / 20
val emergencypos = margin / 2
@@ -115,7 +115,7 @@
format(input.flatMap(standard_format), 0, 0, Text()).content
}
- def string_of(input: List[XML.Tree], margin: Int = default_margin): String =
+ def string_of(input: List[XML.Tree], margin: Int = margin_default): String =
formatted(input).iterator.flatMap(XML.content).mkString
--- a/src/Pure/Isar/class.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/Isar/class.ML Sat May 08 20:14:11 2010 +0200
@@ -202,7 +202,7 @@
|> Expression.cert_declaration supexpr I inferred_elems;
fun check_vars e vs = if null vs
then error ("No type variable in part of specification element "
- ^ (Pretty.output o Pretty.chunks) (Element.pretty_ctxt class_ctxt e))
+ ^ (Pretty.string_of o Pretty.chunks) (Element.pretty_ctxt class_ctxt e))
else ();
fun check_element (e as Element.Fixes fxs) =
map (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs
--- a/src/Pure/Isar/isar_cmd.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Sat May 08 20:14:11 2010 +0200
@@ -313,7 +313,7 @@
(* pretty_setmargin *)
-fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.setmargin n);
+fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.margin_default := n);
(* print parts of theory and proof context *)
--- a/src/Pure/Proof/extraction.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/Proof/extraction.ML Sat May 08 20:14:11 2010 +0200
@@ -303,7 +303,7 @@
val rd = Proof_Syntax.read_proof thy' false;
in fn (thm, (vs, s1, s2)) =>
let
- val name = Thm.get_name thm;
+ val name = Thm.derivation_name thm;
val _ = name <> "" orelse error "add_realizers: unnamed theorem";
val prop = Pattern.rewrite_term thy'
(map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
@@ -348,7 +348,7 @@
val {realizes_eqns, typeof_eqns, types, realizers,
defs, expand, prep} = ExtractionData.get thy;
- val name = Thm.get_name thm;
+ val name = Thm.derivation_name thm;
val _ = name <> "" orelse error "add_expand_thm: unnamed theorem";
in
thy |> ExtractionData.put
@@ -706,7 +706,7 @@
val thy = Thm.theory_of_thm thm;
val prop = Thm.prop_of thm;
val prf = Thm.proof_of thm;
- val name = Thm.get_name thm;
+ val name = Thm.derivation_name thm;
val _ = name <> "" orelse error "extraction: unnamed theorem";
val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
quote name ^ " has no computational content")
--- a/src/Pure/Proof/proof_rewrite_rules.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Sat May 08 20:14:11 2010 +0200
@@ -244,7 +244,7 @@
fun elim_defs thy r defs prf =
let
val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs
- val defnames = map Thm.get_name defs;
+ val defnames = map Thm.derivation_name defs;
val f = if not r then I else
let
val cnames = map (fst o dest_Const o fst) defs';
--- a/src/Pure/Syntax/syntax.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML Sat May 08 20:14:11 2010 +0200
@@ -698,21 +698,23 @@
in (syms, pos) end;
local
- type operations =
- {parse_sort: Proof.context -> string -> sort,
- parse_typ: Proof.context -> string -> typ,
- parse_term: Proof.context -> string -> term,
- parse_prop: Proof.context -> string -> term,
- unparse_sort: Proof.context -> sort -> Pretty.T,
- unparse_typ: Proof.context -> typ -> Pretty.T,
- unparse_term: Proof.context -> term -> Pretty.T};
- val operations = Unsynchronized.ref (NONE: operations option);
+type operations =
+ {parse_sort: Proof.context -> string -> sort,
+ parse_typ: Proof.context -> string -> typ,
+ parse_term: Proof.context -> string -> term,
+ parse_prop: Proof.context -> string -> term,
+ unparse_sort: Proof.context -> sort -> Pretty.T,
+ unparse_typ: Proof.context -> typ -> Pretty.T,
+ unparse_term: Proof.context -> term -> Pretty.T};
- fun operation which ctxt x =
- (case ! operations of
- NONE => error "Inner syntax operations not yet installed"
- | SOME ops => which ops ctxt x);
+val operations: operations Single_Assignment.var = Single_Assignment.var "Syntax.operations";
+
+fun operation which ctxt x =
+ (case Single_Assignment.peek operations of
+ NONE => raise Fail "Inner syntax operations not installed"
+ | SOME ops => which ops ctxt x);
+
in
val parse_sort = operation #parse_sort;
@@ -723,9 +725,7 @@
val unparse_typ = operation #unparse_typ;
val unparse_term = operation #unparse_term;
-fun install_operations ops = CRITICAL (fn () =>
- if is_some (! operations) then error "Inner syntax operations already installed"
- else operations := SOME ops);
+fun install_operations ops = Single_Assignment.assign operations ops;
end;
--- a/src/Pure/Thy/thm_deps.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/Thy/thm_deps.ML Sat May 08 20:14:11 2010 +0200
@@ -53,7 +53,7 @@
else
let val {concealed, group, ...} = Name_Space.the_entry space name in
fold_rev (fn th =>
- (case Thm.get_name th of
+ (case Thm.derivation_name th of
"" => I
| a => cons (a, (th, concealed, group)))) ths
end;
--- a/src/Pure/Thy/thy_output.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML Sat May 08 20:14:11 2010 +0200
@@ -428,7 +428,7 @@
("break", setmp_CRITICAL break o boolean),
("quotes", setmp_CRITICAL quotes o boolean),
("mode", fn s => fn f => PrintMode.with_modes [s] f),
- ("margin", Pretty.setmp_margin_CRITICAL o integer),
+ ("margin", setmp_CRITICAL Pretty.margin_default o integer),
("indent", setmp_CRITICAL indent o integer),
("source", setmp_CRITICAL source o boolean),
("goals_limit", setmp_CRITICAL goals_limit o integer)];
--- a/src/Pure/axclass.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/axclass.ML Sat May 08 20:14:11 2010 +0200
@@ -241,7 +241,7 @@
end;
-fun the_arity thy a (c, Ss) =
+fun the_arity thy (a, Ss, c) =
(case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
SOME (thm, _) => Thm.transfer thy thm
| NONE => error ("Unproven type arity " ^
@@ -295,10 +295,12 @@
end;
val _ = Context.>> (Context.map_theory
- (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities));
+ (Theory.at_begin complete_classrels #>
+ Theory.at_begin complete_arities));
-val the_classrel_prf = Thm.proof_of oo the_classrel;
-val the_arity_prf = Thm.proof_of ooo the_arity;
+val _ = Proofterm.install_axclass_proofs
+ {classrel_proof = Thm.proof_of oo the_classrel,
+ arity_proof = Thm.proof_of oo the_arity};
(* maintain instance parameters *)
--- a/src/Pure/codegen.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/codegen.ML Sat May 08 20:14:11 2010 +0200
@@ -109,9 +109,7 @@
val margin = Unsynchronized.ref 80;
-fun string_of p = (Pretty.string_of |>
- PrintMode.setmp [] |>
- Pretty.setmp_margin_CRITICAL (!margin)) p;
+fun string_of p = PrintMode.setmp [] (Pretty.string_of_margin (!margin)) p;
val str = PrintMode.setmp [] Pretty.str;
--- a/src/Pure/more_thm.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/more_thm.ML Sat May 08 20:14:11 2010 +0200
@@ -326,7 +326,7 @@
(* close_derivation *)
fun close_derivation thm =
- if Thm.get_name thm = "" then Thm.put_name "" thm
+ if Thm.derivation_name thm = "" then Thm.name_derivation "" thm
else thm;
--- a/src/Pure/proofterm.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/proofterm.ML Sat May 08 20:14:11 2010 +0200
@@ -84,7 +84,7 @@
val varify_proof: term -> (string * sort) list -> proof -> proof
val legacy_freezeT: term -> proof -> proof
val rotate_proof: term list -> term -> int -> proof -> proof
- val permute_prems_prf: term list -> int -> int -> proof -> proof
+ val permute_prems_proof: term list -> int -> int -> proof -> proof
val generalize: string list * string list -> int -> proof -> proof
val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
-> proof -> proof
@@ -110,6 +110,12 @@
val equal_elim: term -> term -> proof -> proof -> proof
val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list ->
sort list -> proof -> proof
+ val classrel_proof: theory -> class * class -> proof
+ val arity_proof: theory -> string * sort list * class -> proof
+ val of_sort_proof: theory -> (typ * class -> proof) -> typ * sort -> proof list
+ val install_axclass_proofs:
+ {classrel_proof: theory -> class * class -> proof,
+ arity_proof: theory -> string * sort list * class -> proof} -> unit
val axm_proof: string -> term -> proof
val oracle_proof: string -> term -> oracle * proof
val promise_proof: theory -> serial -> term -> proof
@@ -689,7 +695,7 @@
(***** permute premises *****)
-fun permute_prems_prf prems j k prf =
+fun permute_prems_proof prems j k prf =
let val n = length prems
in mk_AbsP (n, proof_combP (prf,
map PBound ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k))))
@@ -886,7 +892,7 @@
equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
-(**** sort hypotheses ****)
+(**** type classes ****)
fun strip_shyps_proof algebra present witnessed extra_sorts prf =
let
@@ -902,6 +908,53 @@
in Same.commit (map_proof_types_same (Term_Subst.map_atypsT_same replace)) prf end;
+local
+
+type axclass_proofs =
+ {classrel_proof: theory -> class * class -> proof,
+ arity_proof: theory -> string * sort list * class -> proof};
+
+val axclass_proofs: axclass_proofs Single_Assignment.var =
+ Single_Assignment.var "Proofterm.axclass_proofs";
+
+fun axclass_proof which thy x =
+ (case Single_Assignment.peek axclass_proofs of
+ NONE => raise Fail "Axclass proof operations not installed"
+ | SOME prfs => which prfs thy x);
+
+in
+
+val classrel_proof = axclass_proof #classrel_proof;
+val arity_proof = axclass_proof #arity_proof;
+
+fun install_axclass_proofs prfs = Single_Assignment.assign axclass_proofs prfs;
+
+end;
+
+
+local
+
+fun canonical_instance typs =
+ let
+ val names = Name.invents Name.context Name.aT (length typs);
+ val instT = map2 (fn a => fn T => (((a, 0), []), Type.strip_sorts T)) names typs;
+ in instantiate (instT, []) end;
+
+in
+
+fun of_sort_proof thy hyps =
+ Sorts.of_sort_derivation (Sign.classes_of thy)
+ {class_relation = fn typ => fn (prf, c1) => fn c2 =>
+ if c1 = c2 then prf
+ else canonical_instance [typ] (classrel_proof thy (c1, c2)) %% prf,
+ type_constructor = fn (a, typs) => fn dom => fn c =>
+ let val Ss = map (map snd) dom and prfs = maps (map fst) dom
+ in proof_combP (canonical_instance typs (arity_proof thy (a, Ss, c)), prfs) end,
+ type_variable = fn typ => map (fn c => (hyps (typ, c), c)) (Type.sort_of_atyp typ)};
+
+end;
+
+
(***** axioms and theorems *****)
val proofs = Unsynchronized.ref 2;
--- a/src/Pure/pure_thy.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/pure_thy.ML Sat May 08 20:14:11 2010 +0200
@@ -121,7 +121,7 @@
| name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
fun name_thm pre official name thm = thm
- |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name)
+ |> not (Thm.derivation_name thm <> "" andalso pre orelse not official) ? Thm.name_derivation name
|> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name);
fun name_thms pre official name xs =
--- a/src/Pure/thm.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/thm.ML Sat May 08 20:14:11 2010 +0200
@@ -126,8 +126,8 @@
val proof_of: thm -> proof
val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
val future: thm future -> cterm -> thm
- val get_name: thm -> string
- val put_name: string -> thm -> thm
+ val derivation_name: thm -> string
+ val name_derivation: string -> thm -> thm
val axiom: theory -> string -> thm
val axioms_of: theory -> (string * thm) list
val get_tags: thm -> Properties.T
@@ -585,10 +585,10 @@
(* closed derivations with official name *)
-fun get_name thm =
+fun derivation_name thm =
Pt.get_name (hyps_of thm) (prop_of thm) (Pt.proof_of (raw_body thm));
-fun put_name name (thm as Thm (der, args)) =
+fun name_derivation name (thm as Thm (der, args)) =
let
val Deriv {promises, body} = der;
val {thy_ref, hyps, prop, tpairs, ...} = args;
@@ -1436,7 +1436,7 @@
in Logic.list_implies (fixed_prems @ qs @ ps, concl) end
else raise THM ("permute_prems: k", k, [rl]);
in
- Thm (deriv_rule1 (Pt.permute_prems_prf prems j m) der,
+ Thm (deriv_rule1 (Pt.permute_prems_proof prems j m) der,
{thy_ref = thy_ref,
tags = [],
maxidx = maxidx,
--- a/src/Tools/Code/code_printer.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Sat May 08 20:14:11 2010 +0200
@@ -116,8 +116,8 @@
fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
fun indent i = PrintMode.setmp [] (Pretty.indent i);
-fun string_of_pretty width p = PrintMode.setmp [] (Pretty.setmp_margin_CRITICAL width Pretty.string_of) p ^ "\n";
-fun writeln_pretty width p = PrintMode.setmp [] (Pretty.setmp_margin_CRITICAL width Pretty.writeln) p;
+fun string_of_pretty width p = PrintMode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
+fun writeln_pretty width p = writeln (PrintMode.setmp [] (Pretty.string_of_margin width) p);
(** names and variable name contexts **)
--- a/src/Tools/WWW_Find/find_theorems.ML Sat May 08 20:01:28 2010 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML Sat May 08 20:14:11 2010 +0200
@@ -143,7 +143,7 @@
fun html_thm ctxt (n, (thmref, thm)) =
let
val string_of_thm =
- Output.output o Pretty.setmp_margin_CRITICAL 100 Pretty.string_of o
+ Output.output o Pretty.string_of_margin 100 o
setmp_CRITICAL show_question_marks false (Display.pretty_thm ctxt);
in
tag' "tr" (class ("row" ^ Int.toString (n mod 2)))