--- a/NEWS Thu May 27 18:16:54 2010 +0200
+++ b/NEWS Thu May 27 21:37:42 2010 +0200
@@ -504,6 +504,8 @@
OuterParse ~> Parse
OuterSyntax ~> Outer_Syntax
SpecParse ~> Parse_Spec
+ TypeInfer ~> Type_Infer
+ PrintMode ~> Print_Mode
Note that "open Legacy" simplifies porting of sources, but forgetting
to remove it again will complicate porting again in the future.
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Thu May 27 18:16:54 2010 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Thu May 27 21:37:42 2010 +0200
@@ -148,7 +148,7 @@
ML {*
fun check_syntax ctxt thm expected =
let
- val obtained = PrintMode.setmp [] (Display.string_of_thm ctxt) thm;
+ val obtained = Print_Mode.setmp [] (Display.string_of_thm ctxt) thm;
in
if obtained <> expected
then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.")
--- a/src/HOL/Import/proof_kernel.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Thu May 27 21:37:42 2010 +0200
@@ -200,7 +200,7 @@
handle TERM _ => ct)
in
quote (
- PrintMode.setmp [] (
+ Print_Mode.setmp [] (
setmp_CRITICAL show_brackets false (
setmp_CRITICAL show_all_types true (
setmp_CRITICAL Syntax.ambiguity_is_error false (
@@ -229,7 +229,7 @@
val str =
setmp_CRITICAL show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
val u = Syntax.parse_term ctxt str
- |> TypeInfer.constrain T |> Syntax.check_term ctxt
+ |> Type_Infer.constrain T |> Syntax.check_term ctxt
in
if match u
then quote str
@@ -239,14 +239,14 @@
| SMART_STRING =>
error ("smart_string failed for: "^ G 0 (Syntax.string_of_term ctxt o term_of) ct)
in
- PrintMode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0
+ Print_Mode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0
end
handle ERROR mesg => simple_smart_string_of_cterm ct
val smart_string_of_thm = smart_string_of_cterm o cprop_of
-fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th);
-fun prin t = writeln (PrintMode.setmp []
+fun prth th = writeln (Print_Mode.setmp [] Display.string_of_thm_without_context th);
+fun prin t = writeln (Print_Mode.setmp []
(fn () => Syntax.string_of_term (ML_Context.the_local_context ()) t) ());
fun pth (HOLThm(ren,thm)) =
let
--- a/src/HOL/Import/shuffler.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Import/shuffler.ML Thu May 27 21:37:42 2010 +0200
@@ -56,7 +56,7 @@
(*Prints an exception, then fails*)
fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
-val string_of_thm = PrintMode.setmp [] Display.string_of_thm_without_context;
+val string_of_thm = Print_Mode.setmp [] Display.string_of_thm_without_context;
fun mk_meta_eq th =
(case concl_of th of
--- a/src/HOL/Modelcheck/EindhovenSyn.thy Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy Thu May 27 21:37:42 2010 +0200
@@ -32,7 +32,7 @@
oracle mc_eindhoven_oracle =
{*
let
- val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Syntax.string_of_term_global;
+ val eindhoven_term = Print_Mode.setmp ["Eindhoven"] o Syntax.string_of_term_global;
fun call_mc s =
let
--- a/src/HOL/Modelcheck/mucke_oracle.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Thu May 27 21:37:42 2010 +0200
@@ -487,7 +487,7 @@
make_string sign (trm::list) =
Syntax.string_of_term_global sign trm ^ "\n" ^ make_string sign list
in
- PrintMode.setmp ["Mucke"] (make_string sign) terms
+ Print_Mode.setmp ["Mucke"] (make_string sign) terms
end;
fun callmc s =
--- a/src/HOL/Statespace/state_space.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML Thu May 27 21:37:42 2010 +0200
@@ -439,7 +439,7 @@
fun string_of_typ T =
setmp_CRITICAL show_sorts true
- (PrintMode.setmp [] (Syntax.string_of_typ (ProofContext.init_global thy))) T;
+ (Print_Mode.setmp [] (Syntax.string_of_typ (ProofContext.init_global thy))) T;
val fixestate = (case state_type of
NONE => []
| SOME s =>
--- a/src/HOL/Tools/Function/function.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Tools/Function/function.ML Thu May 27 21:37:42 2010 +0200
@@ -149,7 +149,7 @@
end
val add_function =
- gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
+ gen_add_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
val add_function_cmd = gen_add_function true Specification.read_spec "_::type"
fun gen_function is_external prep default_constraint fixspec eqns config lthy =
@@ -163,7 +163,7 @@
end
val function =
- gen_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
+ gen_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
val function_cmd = gen_function true Specification.read_spec "_::type"
fun prepare_termination_proof prep_term raw_term_opt lthy =
--- a/src/HOL/Tools/Function/function_core.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Thu May 27 21:37:42 2010 +0200
@@ -879,7 +879,7 @@
val ranT = range_type fT
val default = Syntax.parse_term lthy default_str
- |> TypeInfer.constrain fT |> Syntax.check_term lthy
+ |> Type_Infer.constrain fT |> Syntax.check_term lthy
val (globals, ctxt') = fix_globals domT ranT fvar lthy
--- a/src/HOL/Tools/Nitpick/nitpick.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu May 27 21:37:42 2010 +0200
@@ -483,7 +483,7 @@
val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True
val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
- PrintMode.setmp [] multiline_string_for_scope scope
+ Print_Mode.setmp [] multiline_string_for_scope scope
val kodkod_sat_solver =
Kodkod_SAT.sat_solver_spec actual_sat_solver |> snd
val bit_width = if bits = 0 then 16 else bits + 1
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu May 27 21:37:42 2010 +0200
@@ -3306,7 +3306,7 @@
Pretty.str "total:", Pretty.brk 1, Pretty.str (string_of_int total), Pretty.fbrk]
@ maps pretty_entry xs
end
- val p = PrintMode.with_modes print_modes (fn () =>
+ val p = Print_Mode.with_modes print_modes (fn () =>
Pretty.block ([Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]
@ pretty_stat)) ();
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu May 27 21:37:42 2010 +0200
@@ -254,7 +254,7 @@
SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
| NONE =>
(* Variable from the ATP, say "X1" *)
- TypeInfer.param 0 (a, HOLogic.typeS)
+ Type_Infer.param 0 (a, HOLogic.typeS)
end
(*Invert the table of translations between Isabelle and ATPs*)
@@ -453,7 +453,7 @@
val (vt, t) = lits_of_nodes thy full_types tfrees (Vartab.empty, []) us
in repair_tvar_sorts vt t end
fun check_formula ctxt =
- TypeInfer.constrain @{typ bool}
+ Type_Infer.constrain @{typ bool}
#> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
@@ -911,7 +911,7 @@
fun string_for_proof ctxt i n =
let
fun fix_print_mode f =
- PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+ Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
(print_mode_value ())) f
fun do_indent ind = replicate_string (ind * indent_size) " "
fun do_free (s, T) =
--- a/src/HOL/Tools/hologic.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Tools/hologic.ML Thu May 27 21:37:42 2010 +0200
@@ -138,7 +138,7 @@
(* HOL syntax *)
val typeS: sort = ["HOL.type"];
-val typeT = TypeInfer.anyT typeS;
+val typeT = Type_Infer.anyT typeS;
(* bool and set *)
--- a/src/HOL/Tools/primrec.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/HOL/Tools/primrec.ML Thu May 27 21:37:42 2010 +0200
@@ -197,7 +197,7 @@
val raw_rhs = fold_rev (fn T => fn t => Abs ("", T, t)) (map snd ls @ [dummyT])
(list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1))))
val rhs = singleton (Syntax.check_terms ctxt)
- (TypeInfer.constrain varT raw_rhs);
+ (Type_Infer.constrain varT raw_rhs);
in (var, ((Binding.conceal (Binding.name def_name), []), rhs)) end;
--- a/src/HOLCF/IOA/meta_theory/automaton.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/automaton.ML Thu May 27 21:37:42 2010 +0200
@@ -18,8 +18,8 @@
structure Automaton: AUTOMATON =
struct
-val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
-val string_of_term = PrintMode.setmp [] o Syntax.string_of_term_global;
+val string_of_typ = Print_Mode.setmp [] o Syntax.string_of_typ_global;
+val string_of_term = Print_Mode.setmp [] o Syntax.string_of_term_global;
exception malformed;
--- a/src/HOLCF/Tools/Domain/domain_library.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Thu May 27 21:37:42 2010 +0200
@@ -185,7 +185,7 @@
fun mk_lam (x,T) = Abs(x,dummyT,T);
fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P);
fun mk_ex (x,P) = mk_exists (x,dummyT,P);
-fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (typ --> boolT) (mk_lam(x,P)));
+fun mk_constrainall (x,typ,P) = %%:"All" $ (Type_Infer.constrain (typ --> boolT) (mk_lam(x,P)));
end
fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Thu May 27 21:37:42 2010 +0200
@@ -463,7 +463,7 @@
fun legacy_infer_term thy t =
singleton (Syntax.check_terms (ProofContext.init_global thy)) (intern_term thy t);
- fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
+ fun legacy_infer_prop thy t = legacy_infer_term thy (Type_Infer.constrain propT t);
fun infer_props thy = map (apsnd (legacy_infer_prop thy));
fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
--- a/src/Pure/General/print_mode.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/General/print_mode.ML Thu May 27 21:37:42 2010 +0200
@@ -22,7 +22,7 @@
val closure: ('a -> 'b) -> 'a -> 'b
end;
-structure PrintMode: PRINT_MODE =
+structure Print_Mode: PRINT_MODE =
struct
val input = "input";
@@ -49,5 +49,5 @@
end;
-structure BasicPrintMode: BASIC_PRINT_MODE = PrintMode;
-open BasicPrintMode;
+structure Basic_Print_Mode: BASIC_PRINT_MODE = Print_Mode;
+open Basic_Print_Mode;
--- a/src/Pure/Isar/class_target.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Isar/class_target.ML Thu May 27 21:37:42 2010 +0200
@@ -275,7 +275,7 @@
of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty
of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
of SOME (_, ty' as TVar (vi, sort)) =>
- if TypeInfer.is_param vi
+ if Type_Infer.is_param vi
andalso Sorts.sort_le algebra (base_sort, sort)
then SOME (ty', TFree (Name.aT, base_sort))
else NONE
@@ -355,7 +355,7 @@
|> snd
|> Sign.add_const_constraint (c', SOME ty')
|> Sign.notation true prmode [(Const (c', ty'), mx)]
- |> not (#1 prmode = PrintMode.input) ? register_operation class (c', (rhs', NONE))
+ |> not (#1 prmode = Print_Mode.input) ? register_operation class (c', (rhs', NONE))
end;
--- a/src/Pure/Isar/expression.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Isar/expression.ML Thu May 27 21:37:42 2010 +0200
@@ -162,9 +162,9 @@
val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
(* type inference and contexts *)
- val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT_global) parm_types;
+ val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types;
val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
- val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
+ val arg = type_parms @ map2 Type_Infer.constrain parm_types' insts';
val res = Syntax.check_terms ctxt arg;
val ctxt' = ctxt |> fold Variable.auto_fixes res;
@@ -345,9 +345,9 @@
let
val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
val inst' = prep_inst ctxt parm_names inst;
- val parm_types' = map (TypeInfer.paramify_vars o
+ val parm_types' = map (Type_Infer.paramify_vars o
Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global) parm_types;
- val inst'' = map2 TypeInfer.constrain parm_types' inst';
+ val inst'' = map2 Type_Infer.constrain parm_types' inst';
val insts' = insts @ [(loc, (prfx, inst''))];
val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
val inst''' = insts'' |> List.last |> snd |> snd;
--- a/src/Pure/Isar/isar_cmd.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Thu May 27 21:37:42 2010 +0200
@@ -281,7 +281,7 @@
fun pr (modes, (lim1, lim2)) = Toplevel.keep (fn state =>
(set_limit goals_limit lim1; set_limit ProofContext.prems_limit lim2; Toplevel.quiet := false;
- PrintMode.with_modes modes (Toplevel.print_state true) state));
+ Print_Mode.with_modes modes (Toplevel.print_state true) state));
val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true);
val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false);
@@ -488,7 +488,7 @@
in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end;
fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
- PrintMode.with_modes modes (fn () =>
+ Print_Mode.with_modes modes (fn () =>
writeln (string_of (Toplevel.enter_proof_body state) arg)) ());
in
--- a/src/Pure/Isar/isar_document.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML Thu May 27 21:37:42 2010 +0200
@@ -111,20 +111,20 @@
(* states *)
-val empty_state = Future.value (SOME Toplevel.toplevel);
+val empty_state = Lazy.value (SOME Toplevel.toplevel);
local
-
-val global_states = Unsynchronized.ref (Symtab.make [(no_id, empty_state)]);
-
+ val global_states = Unsynchronized.ref (Symtab.make [(no_id, empty_state)]);
in
fun define_state (id: state_id) =
- Unsynchronized.change global_states (Symtab.update_new (id, empty_state))
- handle Symtab.DUP dup => err_dup "state" dup;
+ NAMED_CRITICAL "Isar" (fn () =>
+ Unsynchronized.change global_states (Symtab.update_new (id, empty_state))
+ handle Symtab.DUP dup => err_dup "state" dup);
fun put_state (id: state_id) state =
- Unsynchronized.change global_states (Symtab.update (id, state));
+ NAMED_CRITICAL "Isar" (fn () =>
+ Unsynchronized.change global_states (Symtab.update (id, state)));
fun the_state (id: state_id) =
(case Symtab.lookup (! global_states) id of
@@ -137,9 +137,7 @@
(* commands *)
local
-
-val global_commands = Unsynchronized.ref (Symtab.make [(no_id, Toplevel.empty)]);
-
+ val global_commands = Unsynchronized.ref (Symtab.make [(no_id, Toplevel.empty)]);
in
fun define_command id tr =
@@ -158,9 +156,7 @@
(* documents *)
local
-
-val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);
-
+ val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);
in
fun define_document (id: document_id) document =
@@ -176,6 +172,18 @@
end;
+(* execution *)
+
+local
+ val execution = Unsynchronized.ref (Future.value ());
+in
+
+fun execute e =
+ NAMED_CRITICAL "Isar" (fn () => (Future.cancel (! execution); execution := Future.fork e));
+
+end;
+
+
(** main operations **)
@@ -196,9 +204,9 @@
val end_state =
the_state (the (#state (#3 (the
(first_entry (fn (_, {next, ...}) => is_none next) document)))));
- val _ =
- Future.fork_deps [end_state] (fn () =>
- (case Future.join end_state of
+ val _ = (* FIXME regular execution (??) *)
+ Future.fork (fn () =>
+ (case Lazy.force end_state of
SOME st =>
(Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st;
ThyInfo.touch_child_thys name;
@@ -225,11 +233,11 @@
let
val state = the_state state_id;
val state' =
- Future.fork_deps [state] (fn () =>
- (case Future.join state of
+ Lazy.lazy (fn () =>
+ (case Lazy.force state of
NONE => NONE
| SOME st => Toplevel.run_command name tr st));
- in put_state state_id' state' end;
+ in put_state state_id' state'; state' end;
in (state_id', ((id, state_id'), make_state') :: updates) end;
fun report_updates updates =
@@ -246,19 +254,11 @@
val new_document as Document {entries = new_entries, ...} = old_document
|> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits;
- fun cancel_old id = fold_entries id
- (fn (_, {state = SOME state_id, ...}) => K (Future.cancel (the_state state_id)) | _ => K ())
- old_document ();
-
val (updates, new_document') =
(case first_entry (is_changed old_entries) new_document of
- NONE =>
- (case first_entry (is_changed new_entries) old_document of
- NONE => ([], new_document)
- | SOME (_, id, _) => (cancel_old id; ([], new_document)))
+ NONE => ([], new_document)
| SOME (prev, id, _) =>
let
- val _ = cancel_old id;
val prev_state_id = the (#state (the_entry new_entries (the prev)));
val (_, updates) = fold_entries id (new_state name) new_document (prev_state_id, []);
val new_document' = new_document |> map_entries (fold (set_entry_state o #1) updates);
@@ -266,7 +266,8 @@
val _ = define_document new_id new_document';
val _ = report_updates (map #1 updates);
- val _ = List.app (fn (_, run) => run ()) updates;
+ val execs = map (fn (_, make) => make ()) updates;
+ val _ = execute (fn () => List.app (ignore o Lazy.force) execs);
in () end);
end;
--- a/src/Pure/Isar/proof_context.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML Thu May 27 21:37:42 2010 +0200
@@ -577,7 +577,7 @@
pattern orelse schematic orelse
T |> Term.exists_subtype
(fn TVar (xi, _) =>
- not (TypeInfer.is_param xi) andalso
+ not (Type_Infer.is_param xi) andalso
error ("Illegal schematic type variable: " ^ Term.string_of_vname xi)
| _ => false)
in T end;
@@ -599,7 +599,7 @@
fun prepare_patterns ctxt =
let val Mode {pattern, ...} = get_mode ctxt in
- TypeInfer.fixate_params (Variable.names_of ctxt) #>
+ Type_Infer.fixate_params (Variable.names_of ctxt) #>
pattern ? Variable.polymorphic ctxt #>
(map o Term.map_types) (prepare_patternT ctxt) #>
(if pattern then prepare_dummies else map (check_dummies ctxt))
@@ -699,7 +699,7 @@
in Variable.def_type ctxt pattern end;
fun standard_infer_types ctxt ts =
- TypeInfer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
+ Type_Infer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
(try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt)
(Variable.names_of ctxt) (Variable.maxidx_of ctxt) ts
handle TYPE (msg, _, _) => error msg;
@@ -754,11 +754,11 @@
let
val {get_sort, map_const, map_free} = term_context ctxt;
- val (T', _) = TypeInfer.paramify_dummies T 0;
+ val (T', _) = Type_Infer.paramify_dummies T 0;
val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
val (syms, pos) = Syntax.parse_token markup text;
- fun check t = (Syntax.check_term ctxt (TypeInfer.constrain T' t); NONE)
+ fun check t = (Syntax.check_term ctxt (Type_Infer.constrain T' t); NONE)
handle ERROR msg => SOME msg;
val t =
Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
@@ -883,7 +883,7 @@
in
fun read_terms ctxt T =
- map (Syntax.parse_term ctxt #> TypeInfer.constrain T) #> Syntax.check_terms ctxt;
+ map (Syntax.parse_term ctxt #> Type_Infer.constrain T) #> Syntax.check_terms ctxt;
val match_bind = gen_bind read_terms;
val match_bind_i = gen_bind (fn ctxt => fn _ => map (cert_term ctxt));
--- a/src/Pure/Isar/rule_insts.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Isar/rule_insts.ML Thu May 27 21:37:42 2010 +0200
@@ -82,7 +82,7 @@
fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
val ts = map2 parse Ts ss;
val ts' =
- map2 (TypeInfer.constrain o TypeInfer.paramify_vars) Ts ts
+ map2 (Type_Infer.constrain o Type_Infer.paramify_vars) Ts ts
|> Syntax.check_terms ((schematic ? ProofContext.set_mode ProofContext.mode_schematic) ctxt)
|> Variable.polymorphic ctxt;
val Ts' = map Term.fastype_of ts';
--- a/src/Pure/Isar/specification.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Isar/specification.ML Thu May 27 21:37:42 2010 +0200
@@ -96,13 +96,13 @@
(case duplicates (op =) commons of [] => ()
| dups => error ("Duplicate local variables " ^ commas_quote dups));
val frees = rev ((fold o fold_aterms) add_free As (rev commons));
- val types = map (TypeInfer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
+ val types = map (Type_Infer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
val uniform_typing = the o AList.lookup (op =) (frees ~~ types);
fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
| abs_body lev y (t $ u) = abs_body lev y t $ abs_body lev y u
| abs_body lev y (t as Free (x, T)) =
- if x = y then TypeInfer.constrain (uniform_typing x) (TypeInfer.constrain T (Bound lev))
+ if x = y then Type_Infer.constrain (uniform_typing x) (Type_Infer.constrain T (Bound lev))
else t
| abs_body _ _ a = a;
fun close (y, U) B =
--- a/src/Pure/Isar/theory_target.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML Thu May 27 21:37:42 2010 +0200
@@ -200,8 +200,8 @@
in
not (is_class andalso (same_shape orelse class_global)) ?
(Context.mapping_result
- (Sign.add_abbrev PrintMode.internal arg)
- (ProofContext.add_abbrev PrintMode.internal arg)
+ (Sign.add_abbrev Print_Mode.internal arg)
+ (ProofContext.add_abbrev Print_Mode.internal arg)
#-> (fn (lhs' as Const (d, _), _) =>
same_shape ?
(Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
@@ -225,7 +225,7 @@
in
lthy |>
(if is_locale then
- Local_Theory.theory_result (Sign.add_abbrev PrintMode.internal (b, global_rhs))
+ Local_Theory.theory_result (Sign.add_abbrev Print_Mode.internal (b, global_rhs))
#-> (fn (lhs, _) =>
let val lhs' = Term.list_comb (Logic.unvarify_global lhs, xs) in
syntax_declaration ta false (locale_const ta prmode ((b, mx2), lhs')) #>
@@ -235,7 +235,7 @@
Local_Theory.theory
(Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> (fn (lhs, _) =>
Sign.notation true prmode [(lhs, mx3)])))
- |> ProofContext.add_abbrev PrintMode.internal (b, t) |> snd
+ |> ProofContext.add_abbrev Print_Mode.internal (b, t) |> snd
|> Local_Defs.fixed_abbrev ((b, NoSyn), t)
end;
--- a/src/Pure/PIDE/state.scala Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/PIDE/state.scala Thu May 27 21:37:42 2010 +0200
@@ -99,6 +99,11 @@
case _ => state
}
}
+ else if (kind == Markup.FACT_DECL || kind == Markup.LOCAL_FACT_DECL ||
+ kind == Markup.ATTRIBUTE || kind == Markup.FIXED_DECL) {
+ // FIXME usually displaced due to lack of full history support
+ state
+ }
else {
state.add_markup(
command.markup_node(begin - 1, end - 1, Command.HighlightInfo(kind)))
--- a/src/Pure/Proof/proof_syntax.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Thu May 27 21:37:42 2010 +0200
@@ -212,7 +212,7 @@
in
fn ty => fn s =>
(if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s
- |> TypeInfer.constrain ty |> Syntax.check_term ctxt
+ |> Type_Infer.constrain ty |> Syntax.check_term ctxt
end;
fun read_proof thy =
--- a/src/Pure/ProofGeneral/pgip_parser.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML Thu May 27 21:37:42 2010 +0200
@@ -93,7 +93,7 @@
let
val kind = ThySyntax.span_kind span;
val toks = ThySyntax.span_content span;
- val text = implode (map (PrintMode.setmp [] ThySyntax.present_token) toks);
+ val text = implode (map (Print_Mode.setmp [] ThySyntax.present_token) toks);
in
(case kind of
ThySyntax.Command name => parse_command name text
--- a/src/Pure/ROOT.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/ROOT.ML Thu May 27 21:37:42 2010 +0200
@@ -309,6 +309,8 @@
structure OuterParse = Parse;
structure OuterSyntax = Outer_Syntax;
structure SpecParse = Parse_Spec;
+structure TypeInfer = Type_Infer;
+structure PrintMode = Print_Mode;
end;
--- a/src/Pure/Syntax/syntax.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML Thu May 27 21:37:42 2010 +0200
@@ -259,7 +259,7 @@
type mode = string * bool;
val mode_default = ("", true);
-val mode_input = (PrintMode.input, true);
+val mode_input = (Print_Mode.input, true);
(* empty_syntax *)
--- a/src/Pure/Thy/html.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Thy/html.ML Thu May 27 21:37:42 2010 +0200
@@ -42,7 +42,7 @@
(* mode *)
val htmlN = "HTML";
-fun html_mode f x = PrintMode.with_modes [htmlN] f x;
+fun html_mode f x = Print_Mode.with_modes [htmlN] f x;
(* common markup *)
--- a/src/Pure/Thy/thy_output.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML Thu May 27 21:37:42 2010 +0200
@@ -153,7 +153,7 @@
| expand (Antiquote.Antiq (ss, (pos, _))) =
let val (opts, src) = Token.read_antiq lex antiq (ss, pos) in
options opts (fn () => command src state) (); (*preview errors!*)
- PrintMode.with_modes (! modes @ Latex.modes)
+ Print_Mode.with_modes (! modes @ Latex.modes)
(Output.no_warnings_CRITICAL (options opts (fn () => command src state))) ()
end
| expand (Antiquote.Open _) = ""
@@ -429,7 +429,7 @@
("display", setmp_CRITICAL display o boolean),
("break", setmp_CRITICAL break o boolean),
("quotes", setmp_CRITICAL quotes o boolean),
- ("mode", fn s => fn f => PrintMode.with_modes [s] f),
+ ("mode", fn s => fn f => Print_Mode.with_modes [s] f),
("margin", setmp_CRITICAL Pretty.margin_default o integer),
("indent", setmp_CRITICAL indent o integer),
("source", setmp_CRITICAL source o boolean),
@@ -455,7 +455,7 @@
fun pretty_term_typ ctxt (style, t) =
let val t' = style t
- in pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t') t') end;
+ in pretty_term ctxt (Type_Infer.constrain (Term.fastype_of t') t') end;
fun pretty_term_typeof ctxt (style, t) =
Syntax.pretty_typ ctxt (Term.fastype_of (style t));
--- a/src/Pure/codegen.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/codegen.ML Thu May 27 21:37:42 2010 +0200
@@ -109,9 +109,9 @@
val margin = Unsynchronized.ref 80;
-fun string_of p = PrintMode.setmp [] (Pretty.string_of_margin (!margin)) p;
+fun string_of p = Print_Mode.setmp [] (Pretty.string_of_margin (!margin)) p;
-val str = PrintMode.setmp [] Pretty.str;
+val str = Print_Mode.setmp [] Pretty.str;
(**** Mixfix syntax ****)
--- a/src/Pure/consts.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/consts.ML Thu May 27 21:37:42 2010 +0200
@@ -270,7 +270,7 @@
let
val cert_term = certify pp tsig false consts;
val expand_term = certify pp tsig true consts;
- val force_expand = mode = PrintMode.internal;
+ val force_expand = mode = Print_Mode.internal;
val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
error ("Illegal schematic variables on rhs of abbreviation " ^ quote (Binding.str_of b));
--- a/src/Pure/old_goals.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/old_goals.ML Thu May 27 21:37:42 2010 +0200
@@ -223,7 +223,7 @@
|> ProofContext.allow_dummies
|> ProofContext.set_mode ProofContext.mode_schematic;
val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
- in parse ctxt s |> TypeInfer.constrain T |> Syntax.check_term ctxt end;
+ in parse ctxt s |> Type_Infer.constrain T |> Syntax.check_term ctxt end;
fun read_term thy = simple_read_term thy dummyT;
fun read_prop thy = simple_read_term thy propT;
--- a/src/Pure/sign.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/sign.ML Thu May 27 21:37:42 2010 +0200
@@ -271,7 +271,7 @@
val t' = subst_bounds (xs, t);
val u' = subst_bounds (xs, u);
val msg = cat_lines
- (TypeInfer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
+ (Type_Infer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
in raise TYPE (msg, [T, U], [t', u']) end;
fun typ_of (_, Const (_, T)) = T
--- a/src/Pure/type_infer.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/type_infer.ML Thu May 27 21:37:42 2010 +0200
@@ -20,7 +20,7 @@
term list -> term list
end;
-structure TypeInfer: TYPE_INFER =
+structure Type_Infer: TYPE_INFER =
struct
--- a/src/Pure/variable.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Pure/variable.ML Thu May 27 21:37:42 2010 +0200
@@ -168,7 +168,7 @@
(case Vartab.lookup types xi of
NONE =>
if pattern then NONE
- else Vartab.lookup binds xi |> Option.map (TypeInfer.polymorphicT o #1)
+ else Vartab.lookup binds xi |> Option.map (Type_Infer.polymorphicT o #1)
| some => some)
end;
--- a/src/Tools/Code/code_printer.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Thu May 27 21:37:42 2010 +0200
@@ -105,19 +105,19 @@
infixr 5 @|;
fun x @@ y = [x, y];
fun xs @| y = xs @ [y];
-val str = PrintMode.setmp [] Pretty.str;
+val str = Print_Mode.setmp [] Pretty.str;
val concat = Pretty.block o Pretty.breaks;
-fun enclose l r = PrintMode.setmp [] (Pretty.enclose l r);
+fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r);
val brackets = enclose "(" ")" o Pretty.breaks;
-fun enum sep l r = PrintMode.setmp [] (Pretty.enum sep l r);
+fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r);
fun enum_default default sep l r [] = str default
| enum_default default sep l r xs = enum sep l r xs;
fun semicolon ps = Pretty.block [concat ps, str ";"];
fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
-fun indent i = PrintMode.setmp [] (Pretty.indent i);
+fun indent i = Print_Mode.setmp [] (Pretty.indent i);
-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);
+fun string_of_pretty width p = Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
+fun writeln_pretty width p = writeln (Print_Mode.setmp [] (Pretty.string_of_margin width) p);
(** names and variable name contexts **)
--- a/src/Tools/WWW_Find/html_unicode.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Tools/WWW_Find/html_unicode.ML Thu May 27 21:37:42 2010 +0200
@@ -19,7 +19,7 @@
(* mode *)
val htmlunicodeN = "HTMLUnicode";
-fun print_mode f x = PrintMode.with_modes [htmlunicodeN, Symbol.xsymbolsN] f x;
+fun print_mode f x = Print_Mode.with_modes [htmlunicodeN, Symbol.xsymbolsN] f x;
(* symbol output *)
--- a/src/Tools/nbe.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Tools/nbe.ML Thu May 27 21:37:42 2010 +0200
@@ -506,7 +506,7 @@
val ts' = take_until is_dict ts;
val c = const_of_idx idx;
val T = map_type_tvar (fn ((v, i), _) =>
- TypeInfer.param typidx (v ^ string_of_int i, []))
+ Type_Infer.param typidx (v ^ string_of_int i, []))
(Sign.the_const_type thy c);
val typidx' = typidx + 1;
in of_apps bounds (Term.Const (c, T), ts') typidx' end
@@ -548,9 +548,9 @@
let
val ty' = typ_of_itype program vs0 ty;
fun type_infer t =
- singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
+ singleton (Type_Infer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
(try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
- (TypeInfer.constrain ty' t);
+ (Type_Infer.constrain ty' t);
fun check_tvars t = if null (Term.add_tvars t []) then t else
error ("Illegal schematic type variables in normalized term: "
^ setmp_CRITICAL show_types true (Syntax.string_of_term_global thy) t);
@@ -620,7 +620,7 @@
val t' = norm thy t;
val ty' = Term.type_of t';
val ctxt' = Variable.auto_fixes t ctxt;
- val p = PrintMode.with_modes modes (fn () =>
+ val p = Print_Mode.with_modes modes (fn () =>
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
in Pretty.writeln p end;
--- a/src/Tools/value.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/Tools/value.ML Thu May 27 21:37:42 2010 +0200
@@ -47,7 +47,7 @@
| SOME name => value_select name ctxt t;
val ty' = Term.type_of t';
val ctxt' = Variable.auto_fixes t' ctxt;
- val p = PrintMode.with_modes modes (fn () =>
+ val p = Print_Mode.with_modes modes (fn () =>
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
in Pretty.writeln p end;
--- a/src/ZF/Tools/datatype_package.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/ZF/Tools/datatype_package.ML Thu May 27 21:37:42 2010 +0200
@@ -403,7 +403,7 @@
let
val ctxt = ProofContext.init_global thy;
fun read_is strs =
- map (Syntax.parse_term ctxt #> TypeInfer.constrain @{typ i}) strs
+ map (Syntax.parse_term ctxt #> Type_Infer.constrain @{typ i}) strs
|> Syntax.check_terms ctxt;
val rec_tms = read_is srec_tms;
--- a/src/ZF/Tools/inductive_package.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML Thu May 27 21:37:42 2010 +0200
@@ -555,7 +555,7 @@
(raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
let
val ctxt = ProofContext.init_global thy;
- val read_terms = map (Syntax.parse_term ctxt #> TypeInfer.constrain Ind_Syntax.iT)
+ val read_terms = map (Syntax.parse_term ctxt #> Type_Infer.constrain Ind_Syntax.iT)
#> Syntax.check_terms ctxt;
val intr_atts = map (map (Attrib.attribute thy) o snd) intr_srcs;
--- a/src/ZF/ind_syntax.ML Thu May 27 18:16:54 2010 +0200
+++ b/src/ZF/ind_syntax.ML Thu May 27 21:37:42 2010 +0200
@@ -66,7 +66,7 @@
(*read a constructor specification*)
fun read_construct ctxt (id: string, sprems, syn: mixfix) =
- let val prems = map (Syntax.parse_term ctxt #> TypeInfer.constrain FOLogic.oT) sprems
+ let val prems = map (Syntax.parse_term ctxt #> Type_Infer.constrain FOLogic.oT) sprems
|> Syntax.check_terms ctxt
val args = map (#1 o dest_mem) prems
val T = (map (#2 o dest_Free) args) ---> iT