# HG changeset patch # User bulwahn # Date 1256658447 -3600 # Node ID cb3908614f7e516501a3fb6c73761f31320792eb # Parent f8d43d5215c21562c01bfceba3c39897ecccadfd# Parent 66eddea44a67d33c64df04b994335c471edf434e merged diff -r f8d43d5215c2 -r cb3908614f7e src/HOL/Library/Code_Char.thy --- a/src/HOL/Library/Code_Char.thy Tue Oct 27 16:01:38 2009 +0100 +++ b/src/HOL/Library/Code_Char.thy Tue Oct 27 16:47:27 2009 +0100 @@ -35,4 +35,28 @@ code_const "Code_Evaluation.term_of \ char \ term" (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))") + +definition implode :: "string \ String.literal" where + "implode = STR" + +primrec explode :: "String.literal \ string" where + "explode (STR s) = s" + +lemma [code]: + "literal_case f s = f (explode s)" + "literal_rec f s = f (explode s)" + by (cases s, simp)+ + +code_reserved SML String + +code_const implode + (SML "String.implode") + (OCaml "failwith/ \"implode\"") + (Haskell "_") + +code_const explode + (SML "String.explode") + (OCaml "failwith/ \"explode\"") + (Haskell "_") + end diff -r f8d43d5215c2 -r cb3908614f7e src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Tue Oct 27 16:01:38 2009 +0100 +++ b/src/HOL/Nitpick.thy Tue Oct 27 16:47:27 2009 +0100 @@ -28,7 +28,6 @@ typedecl bisim_iterator -(* FIXME: use axiomatization (here and elsewhere) *) axiomatization unknown :: 'a and undefined_fast_The :: 'a and undefined_fast_Eps :: 'a diff -r f8d43d5215c2 -r cb3908614f7e src/HOL/Random.thy --- a/src/HOL/Random.thy Tue Oct 27 16:01:38 2009 +0100 +++ b/src/HOL/Random.thy Tue Oct 27 16:47:27 2009 +0100 @@ -12,15 +12,15 @@ subsection {* Auxiliary functions *} +fun log :: "code_numeral \ code_numeral \ code_numeral" where + "log b i = (if b \ 1 \ i < b then 1 else 1 + log b (i div b))" + definition inc_shift :: "code_numeral \ code_numeral \ code_numeral" where "inc_shift v k = (if v = k then 1 else k + 1)" definition minus_shift :: "code_numeral \ code_numeral \ code_numeral \ code_numeral" where "minus_shift r k l = (if k < l then r + k - l else k - l)" -fun log :: "code_numeral \ code_numeral \ code_numeral" where - "log b i = (if b \ 1 \ i < b then 1 else 1 + log b (i div b))" - subsection {* Random seeds *} @@ -29,28 +29,19 @@ primrec "next" :: "seed \ code_numeral \ seed" where "next (v, w) = (let k = v div 53668; - v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211); + v' = minus_shift 2147483563 ((v mod 53668) * 40014) (k * 12211); l = w div 52774; - w' = minus_shift 2147483399 (40692 * (w mod 52774)) (l * 3791); + w' = minus_shift 2147483399 ((w mod 52774) * 40692) (l * 3791); z = minus_shift 2147483562 v' (w' + 1) + 1 in (z, (v', w')))" -lemma next_not_0: - "fst (next s) \ 0" - by (cases s) (auto simp add: minus_shift_def Let_def) - -primrec seed_invariant :: "seed \ bool" where - "seed_invariant (v, w) \ 0 < v \ v < 9438322952 \ 0 < w \ True" - definition split_seed :: "seed \ seed \ seed" where "split_seed s = (let (v, w) = s; (v', w') = snd (next s); v'' = inc_shift 2147483562 v; - s'' = (v'', w'); - w'' = inc_shift 2147483398 w; - s''' = (v', w'') - in (s'', s'''))" + w'' = inc_shift 2147483398 w + in ((v'', w'), (v', w'')))" subsection {* Base selectors *} @@ -175,7 +166,7 @@ *} hide (open) type seed -hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed +hide (open) const inc_shift minus_shift log "next" split_seed iterate range select pick select_weight no_notation fcomp (infixl "o>" 60) diff -r f8d43d5215c2 -r cb3908614f7e src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Tue Oct 27 16:01:38 2009 +0100 +++ b/src/HOL/Statespace/state_space.ML Tue Oct 27 16:47:27 2009 +0100 @@ -297,7 +297,7 @@ val tt' = tt |> fold upd all_names; val activate_simproc = - Output.no_warnings_CRITICAL + Output.no_warnings_CRITICAL (* FIXME !?! *) (Simplifier.map_ss (fn ss => ss addsimprocs [distinct_simproc])); val ctxt' = ctxt diff -r f8d43d5215c2 -r cb3908614f7e src/HOL/String.thy --- a/src/HOL/String.thy Tue Oct 27 16:01:38 2009 +0100 +++ b/src/HOL/String.thy Tue Oct 27 16:47:27 2009 +0100 @@ -155,7 +155,7 @@ datatype literal = STR string -lemmas [code del] = literal.recs literal.cases +declare literal.cases [code del] literal.recs [code del] lemma [code]: "size (s\literal) = 0" by (cases s) simp_all @@ -168,6 +168,9 @@ use "Tools/string_code.ML" +code_reserved SML string +code_reserved OCaml string + code_type literal (SML "string") (OCaml "string") @@ -185,9 +188,6 @@ (OCaml "!((_ : string) = _)") (Haskell infixl 4 "==") -code_reserved SML string -code_reserved OCaml string - types_code "char" ("string") diff -r f8d43d5215c2 -r cb3908614f7e src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Oct 27 16:01:38 2009 +0100 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Oct 27 16:47:27 2009 +0100 @@ -157,6 +157,7 @@ type raw_bound = n_ary_index * int list list datatype outcome = + NotInstalled | Normal of (int * raw_bound list) list * int list | TimedOut of int list | Interrupted of int list option | @@ -301,6 +302,7 @@ type raw_bound = n_ary_index * int list list datatype outcome = + NotInstalled | Normal of (int * raw_bound list) list * int list | TimedOut of int list | Interrupted of int list option | @@ -1069,6 +1071,10 @@ if null ps then if code = 2 then TimedOut js + else if first_error |> Substring.full + |> Substring.position "NoClassDefFoundError" |> snd + |> Substring.isEmpty |> not then + NotInstalled else if first_error <> "" then Error (first_error |> perhaps (try (unsuffix ".")) |> perhaps (try (unprefix "Error: ")), js) diff -r f8d43d5215c2 -r cb3908614f7e src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Oct 27 16:01:38 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Oct 27 16:47:27 2009 +0100 @@ -626,7 +626,18 @@ else case Kodkod.solve_any_problem overlord deadline max_threads max_solutions (map fst problems) of - Kodkod.Normal ([], unsat_js) => + Kodkod.NotInstalled => + (print_m (fn () => + "Nitpick requires the external Java program Kodkodi. \ + \To install it, download the package from Isabelle's \ + \web page and add the \"kodkodi-x.y.z\" directory's \ + \full path to \"" ^ + Path.implode (Path.expand (Path.appends + (Path.variable "ISABELLE_HOME" :: + (map Path.basic ["etc", "components"])))) ^ + "\"."); + (max_potential, max_genuine, donno + 1)) + | Kodkod.Normal ([], unsat_js) => (update_checked_problems problems unsat_js; (max_potential, max_genuine, donno)) | Kodkod.Normal (sat_ps, unsat_js) => @@ -785,7 +796,7 @@ (* int -> int -> scope list -> int * int * int -> Kodkod.outcome *) fun run_batches _ _ [] (max_potential, max_genuine, donno) = if donno > 0 andalso max_genuine > 0 then - (print_m (fn () => excipit "ran out of resources"); "unknown") + (print_m (fn () => excipit "ran into difficulties"); "unknown") else if max_genuine = original_max_genuine then if max_potential = original_max_potential then (print_m (K ("Nitpick found no " ^ word_model ^ ".")); "none") diff -r f8d43d5215c2 -r cb3908614f7e src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Tue Oct 27 16:01:38 2009 +0100 +++ b/src/HOL/Tools/meson.ML Tue Oct 27 16:47:27 2009 +0100 @@ -323,7 +323,7 @@ Strips universal quantifiers and breaks up conjunctions. Eliminates existential quantifiers using skoths: Skolemization theorems.*) fun cnf skoths ctxt (th,ths) = - let val ctxtr = Unsynchronized.ref ctxt + let val ctxtr = Unsynchronized.ref ctxt (* FIXME ??? *) fun cnf_aux (th,ths) = if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*) else if not (has_conns ["All","Ex","op &"] (prop_of th)) diff -r f8d43d5215c2 -r cb3908614f7e src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Tue Oct 27 16:01:38 2009 +0100 +++ b/src/HOL/Tools/res_axioms.ML Tue Oct 27 16:47:27 2009 +0100 @@ -71,7 +71,7 @@ prefix for the Skolem constant.*) fun declare_skofuns s th = let - val nref = Unsynchronized.ref 0 + val nref = Unsynchronized.ref 0 (* FIXME ??? *) fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) = (*Existential: declare a Skolem function, then insert into body and continue*) let @@ -87,7 +87,8 @@ val (c, thy') = Sign.declare_const ((Binding.conceal (Binding.name cname), cT), NoSyn) thy val cdef = cname ^ "_def" - val thy'' = Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy' + val thy'' = + Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy' val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef) in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end | dec_sko (Const ("All", _) $ (Abs (a, T, p))) thx = @@ -102,7 +103,7 @@ (*Traverse a theorem, accumulating Skolem function definitions.*) fun assume_skofuns s th = - let val sko_count = Unsynchronized.ref 0 + let val sko_count = Unsynchronized.ref 0 (* FIXME ??? *) fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs = (*Existential: declare a Skolem function, then insert into body and continue*) let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*) diff -r f8d43d5215c2 -r cb3908614f7e src/HOLCF/Tools/pcpodef.ML --- a/src/HOLCF/Tools/pcpodef.ML Tue Oct 27 16:01:38 2009 +0100 +++ b/src/HOLCF/Tools/pcpodef.ML Tue Oct 27 16:47:27 2009 +0100 @@ -90,6 +90,7 @@ fun make_cpo admissible (type_def, below_def, set_def) theory = let + (* FIXME fold_rule might fold user input inintentionally *) val admissible' = fold_rule (the_list set_def) admissible; val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible']; val theory' = theory @@ -112,6 +113,7 @@ fun make_pcpo UU_mem (type_def, below_def, set_def) theory = let + (* FIXME fold_rule might fold user input inintentionally *) val UU_mem' = fold_rule (the_list set_def) UU_mem; val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem']; val theory' = theory diff -r f8d43d5215c2 -r cb3908614f7e src/Pure/General/file.ML --- a/src/Pure/General/file.ML Tue Oct 27 16:01:38 2009 +0100 +++ b/src/Pure/General/file.ML Tue Oct 27 16:47:27 2009 +0100 @@ -90,10 +90,10 @@ Unsynchronized.ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table); in -fun check_cache (path, time) = CRITICAL (fn () => +fun check_cache (path, time) = (case Symtab.lookup (! ident_cache) path of NONE => NONE - | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE)); + | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE); fun update_cache (path, (time, id)) = CRITICAL (fn () => Unsynchronized.change ident_cache diff -r f8d43d5215c2 -r cb3908614f7e src/Pure/General/print_mode.ML --- a/src/Pure/General/print_mode.ML Tue Oct 27 16:01:38 2009 +0100 +++ b/src/Pure/General/print_mode.ML Tue Oct 27 16:47:27 2009 +0100 @@ -35,7 +35,7 @@ let val modes = (case Thread.getLocal tag of SOME (SOME modes) => modes - | _ => NAMED_CRITICAL "print_mode" (fn () => ! print_mode)) + | _ => ! print_mode) in subtract (op =) [input, internal] modes end; fun print_mode_active mode = member (op =) (print_mode_value ()) mode; diff -r f8d43d5215c2 -r cb3908614f7e src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Tue Oct 27 16:01:38 2009 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Tue Oct 27 16:47:27 2009 +0100 @@ -333,14 +333,14 @@ Toplevel.keep (ProofContext.print_abbrevs o Toplevel.context_of); val print_facts = Toplevel.unknown_context o Toplevel.keep (fn state => - ProofContext.setmp_verbose + ProofContext.setmp_verbose_CRITICAL ProofContext.print_lthms (Toplevel.context_of state)); val print_configs = Toplevel.unknown_context o Toplevel.keep (fn state => Attrib.print_configs (Toplevel.context_of state)); val print_theorems_proof = Toplevel.keep (fn state => - ProofContext.setmp_verbose + ProofContext.setmp_verbose_CRITICAL ProofContext.print_lthms (Proof.context_of (Toplevel.proof_of state))); val print_theorems_theory = Toplevel.keep (fn state => @@ -431,10 +431,10 @@ (* print proof context contents *) val print_binds = Toplevel.unknown_context o Toplevel.keep (fn state => - ProofContext.setmp_verbose ProofContext.print_binds (Toplevel.context_of state)); + ProofContext.setmp_verbose_CRITICAL ProofContext.print_binds (Toplevel.context_of state)); val print_cases = Toplevel.unknown_context o Toplevel.keep (fn state => - ProofContext.setmp_verbose ProofContext.print_cases (Toplevel.context_of state)); + ProofContext.setmp_verbose_CRITICAL ProofContext.print_cases (Toplevel.context_of state)); (* print theorems, terms, types etc. *) diff -r f8d43d5215c2 -r cb3908614f7e src/Pure/Isar/isar_document.ML --- a/src/Pure/Isar/isar_document.ML Tue Oct 27 16:01:38 2009 +0100 +++ b/src/Pure/Isar/isar_document.ML Tue Oct 27 16:47:27 2009 +0100 @@ -119,13 +119,13 @@ in fun change_states f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_states f); -fun get_states () = NAMED_CRITICAL "Isar" (fn () => ! global_states); +fun get_states () = ! global_states; fun change_commands f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_commands f); -fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands); +fun get_commands () = ! global_commands; fun change_documents f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_documents f); -fun get_documents () = NAMED_CRITICAL "Isar" (fn () => ! global_documents); +fun get_documents () = ! global_documents; fun init () = NAMED_CRITICAL "Isar" (fn () => (global_states := Symtab.empty; diff -r f8d43d5215c2 -r cb3908614f7e src/Pure/Isar/outer_keyword.ML --- a/src/Pure/Isar/outer_keyword.ML Tue Oct 27 16:01:38 2009 +0100 +++ b/src/Pure/Isar/outer_keyword.ML Tue Oct 27 16:47:27 2009 +0100 @@ -121,8 +121,8 @@ in -fun get_commands () = CRITICAL (fn () => ! global_commands); -fun get_lexicons () = CRITICAL (fn () => ! global_lexicons); +fun get_commands () = ! global_commands; +fun get_lexicons () = ! global_lexicons; fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f); fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f); diff -r f8d43d5215c2 -r cb3908614f7e src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Tue Oct 27 16:01:38 2009 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Tue Oct 27 16:47:27 2009 +0100 @@ -101,8 +101,8 @@ (* access current syntax *) -fun get_commands () = CRITICAL (fn () => ! global_commands); -fun get_markups () = CRITICAL (fn () => ! global_markups); +fun get_commands () = ! global_commands; +fun get_markups () = ! global_markups; fun get_command () = Symtab.lookup (get_commands ()); fun get_syntax () = CRITICAL (fn () => (OuterKeyword.get_lexicons (), get_command ())); diff -r f8d43d5215c2 -r cb3908614f7e src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Oct 27 16:01:38 2009 +0100 +++ b/src/Pure/Isar/proof_context.ML Tue Oct 27 16:47:27 2009 +0100 @@ -122,7 +122,7 @@ val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context val revert_abbrev: string -> string -> Proof.context -> Proof.context val verbose: bool Unsynchronized.ref - val setmp_verbose: ('a -> 'b) -> 'a -> 'b + val setmp_verbose_CRITICAL: ('a -> 'b) -> 'a -> 'b val print_syntax: Proof.context -> unit val print_abbrevs: Proof.context -> unit val print_binds: Proof.context -> unit @@ -1200,7 +1200,7 @@ val verbose = Unsynchronized.ref false; fun verb f x = if ! verbose then f (x ()) else []; -fun setmp_verbose f x = setmp_CRITICAL verbose true f x; +fun setmp_verbose_CRITICAL f x = setmp_CRITICAL verbose true f x; (* local syntax *) diff -r f8d43d5215c2 -r cb3908614f7e src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Tue Oct 27 16:01:38 2009 +0100 +++ b/src/Pure/Isar/toplevel.ML Tue Oct 27 16:47:27 2009 +0100 @@ -552,7 +552,7 @@ local val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list) in fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f)); -fun get_hooks () = CRITICAL (fn () => ! hooks); +fun get_hooks () = ! hooks; end; diff -r f8d43d5215c2 -r cb3908614f7e src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Tue Oct 27 16:01:38 2009 +0100 +++ b/src/Pure/ML/ml_context.ML Tue Oct 27 16:47:27 2009 +0100 @@ -54,7 +54,7 @@ (* theorem bindings *) -val stored_thms: thm list Unsynchronized.ref = Unsynchronized.ref []; +val stored_thms: thm list Unsynchronized.ref = Unsynchronized.ref []; (* FIXME via context!? *) fun ml_store sel (name, ths) = let @@ -195,6 +195,7 @@ fun eval_in ctxt verbose pos txt = Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval verbose pos txt) (); +(* FIXME not thread-safe -- reference can be accessed directly *) fun evaluate ctxt verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () => let val _ = r := NONE; diff -r f8d43d5215c2 -r cb3908614f7e src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Tue Oct 27 16:01:38 2009 +0100 +++ b/src/Pure/System/isabelle_process.ML Tue Oct 27 16:47:27 2009 +0100 @@ -61,9 +61,6 @@ else message_pos ts | _ => NONE); -fun output out_stream s = NAMED_CRITICAL "IO" (fn () => - (TextIO.output (out_stream, s); TextIO.output (out_stream, "\n"))); - in fun message _ _ "" = () @@ -74,14 +71,16 @@ Position.properties_of (Position.thread_data ()) |> Position.default_properties pos; val txt = clean_string [Symbol.STX] body; - in output out_stream (special ch ^ message_props props ^ txt ^ special_end) end; + val msg = special ch ^ message_props props ^ txt ^ special_end ^ "\n"; + in TextIO.output (out_stream, msg) end; fun init_message out_stream = let val pid = (Markup.pidN, process_id ()); val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown"); val text = Session.welcome (); - in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end; + val msg = special "A" ^ message_props [pid, session] ^ text ^ special_end ^ "\n"; + in TextIO.output (out_stream, msg) end; end; diff -r f8d43d5215c2 -r cb3908614f7e src/Pure/System/isar.ML --- a/src/Pure/System/isar.ML Tue Oct 27 16:01:38 2009 +0100 +++ b/src/Pure/System/isar.ML Tue Oct 27 16:47:27 2009 +0100 @@ -47,10 +47,10 @@ | edit n (st, hist) = edit (n - 1) (f st hist); in edit count (! global_state, ! global_history) end); -fun state () = NAMED_CRITICAL "Isar" (fn () => ! global_state); +fun state () = ! global_state; -fun exn () = NAMED_CRITICAL "Isar" (fn () => ! global_exn); -fun set_exn exn = NAMED_CRITICAL "Isar" (fn () => global_exn := exn); +fun exn () = ! global_exn; +fun set_exn exn = global_exn := exn; end; diff -r f8d43d5215c2 -r cb3908614f7e src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Tue Oct 27 16:01:38 2009 +0100 +++ b/src/Pure/Thy/html.ML Tue Oct 27 16:47:27 2009 +0100 @@ -267,7 +267,7 @@ (* document *) val charset = Unsynchronized.ref "ISO-8859-1"; -fun with_charset s = setmp_noncritical charset s; (* FIXME *) +fun with_charset s = setmp_noncritical charset s; (* FIXME unreliable *) fun begin_document title = let val cs = ! charset in diff -r f8d43d5215c2 -r cb3908614f7e src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Tue Oct 27 16:01:38 2009 +0100 +++ b/src/Pure/Thy/thy_load.ML Tue Oct 27 16:47:27 2009 +0100 @@ -41,16 +41,22 @@ fun show_path () = map Path.implode (! load_path); -fun del_path s = CRITICAL (fn () => - Unsynchronized.change load_path (remove (op =) (Path.explode s))); -fun add_path s = CRITICAL (fn () => - (del_path s; Unsynchronized.change load_path (cons (Path.explode s)))); -fun path_add s = CRITICAL (fn () => +fun del_path s = + CRITICAL (fn () => Unsynchronized.change load_path (remove (op =) (Path.explode s))); + +fun add_path s = + CRITICAL (fn () => (del_path s; Unsynchronized.change load_path (cons (Path.explode s)))); + +fun path_add s = + CRITICAL (fn () => (del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s]))); + fun reset_path () = load_path := [Path.current]; fun with_paths ss f x = - CRITICAL (fn () => setmp_CRITICAL load_path (! load_path @ map Path.explode ss) f x); + CRITICAL (fn () => + setmp_CRITICAL load_path (! load_path @ map Path.explode ss) f x); + fun with_path s f x = with_paths [s] f x; fun search_path dir path = diff -r f8d43d5215c2 -r cb3908614f7e src/Pure/codegen.ML --- a/src/Pure/codegen.ML Tue Oct 27 16:01:38 2009 +0100 +++ b/src/Pure/codegen.ML Tue Oct 27 16:47:27 2009 +0100 @@ -105,7 +105,7 @@ val quiet_mode = Unsynchronized.ref true; fun message s = if !quiet_mode then () else writeln s; -val mode = Unsynchronized.ref ([] : string list); +val mode = Unsynchronized.ref ([] : string list); (* FIXME proper functional argument *) val margin = Unsynchronized.ref 80; @@ -928,7 +928,7 @@ [str "(result ())"], str ");"]) ^ "\n\nend;\n"; - val _ = NAMED_CRITICAL "codegen" (fn () => + val _ = NAMED_CRITICAL "codegen" (fn () => (* FIXME ??? *) ML_Context.eval_in (SOME ctxt) false Position.none s); in !eval_result end; in e () end;