added compatibility file for ML systems without multithreading;
authorwenzelm
Mon Jul 23 14:06:11 2007 +0200 (2007-07-23)
changeset 23921947152add153
parent 23920 4288dc7dc248
child 23922 707639e9497d
added compatibility file for ML systems without multithreading;
src/Pure/IsaMakefile
src/Pure/ML-Systems/alice.ML
src/Pure/ML-Systems/mosml.ML
src/Pure/ML-Systems/no_multithreading.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/Thy/thm_database.ML
     1.1 --- a/src/Pure/IsaMakefile	Mon Jul 23 13:50:31 2007 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Mon Jul 23 14:06:11 2007 +0200
     1.3 @@ -40,7 +40,8 @@
     1.4    Isar/proof_display.ML Isar/proof_history.ML Isar/rule_cases.ML		\
     1.5    Isar/rule_insts.ML Isar/session.ML Isar/skip_proof.ML Isar/spec_parse.ML	\
     1.6    Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML			\
     1.7 -  ML-Systems/alice.ML ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML	\
     1.8 +  ML-Systems/alice.ML ML-Systems/no_multithreading.ML 				\
     1.9 +  ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML				\
    1.10    ML-Systems/polyml-5.0.ML ML-Systems/polyml-interrupt-timeout.ML		\
    1.11    ML-Systems/polyml-old-basis.ML ML-Systems/polyml-posix.ML 			\
    1.12    ML-Systems/polyml.ML ML-Systems/poplogml.ML ML-Systems/smlnj.ML		\
     2.1 --- a/src/Pure/ML-Systems/alice.ML	Mon Jul 23 13:50:31 2007 +0200
     2.2 +++ b/src/Pure/ML-Systems/alice.ML	Mon Jul 23 14:06:11 2007 +0200
     2.3 @@ -13,6 +13,9 @@
     2.4  - Session.finish ();
     2.5  *)
     2.6  
     2.7 +use "ML-Systems/no_multithreading.ML";
     2.8 +
     2.9 +
    2.10  fun exit 0 = (OS.Process.exit OS.Process.success): unit
    2.11    | exit _ = OS.Process.exit OS.Process.failure;
    2.12  
     3.1 --- a/src/Pure/ML-Systems/mosml.ML	Mon Jul 23 13:50:31 2007 +0200
     3.2 +++ b/src/Pure/ML-Systems/mosml.ML	Mon Jul 23 14:06:11 2007 +0200
     3.3 @@ -29,6 +29,9 @@
     3.4  load "FileSys";
     3.5  load "IO";
     3.6  
     3.7 +use "ML-Systems/no_multithreading.ML";
     3.8 +
     3.9 +
    3.10  (*low-level pointer equality*)
    3.11  local val cast : 'a -> int = Obj.magic
    3.12  in fun pointer_eq (x:'a, y:'a) = (cast x = cast y) end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/ML-Systems/no_multithreading.ML	Mon Jul 23 14:06:11 2007 +0200
     4.3 @@ -0,0 +1,10 @@
     4.4 +(*  Title:      Pure/ML-Systems/no_multithreading.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Makarius
     4.7 +
     4.8 +Compatibility file for ML systems without multithreading.
     4.9 +*)
    4.10 +
    4.11 +(* critical section *)
    4.12 +
    4.13 +fun CRITICAL e = e ();
     5.1 --- a/src/Pure/ML-Systems/polyml.ML	Mon Jul 23 13:50:31 2007 +0200
     5.2 +++ b/src/Pure/ML-Systems/polyml.ML	Mon Jul 23 14:06:11 2007 +0200
     5.3 @@ -4,6 +4,9 @@
     5.4  Compatibility file for Poly/ML (version 4.1.x and 4.2.0).
     5.5  *)
     5.6  
     5.7 +use "ML-Systems/no_multithreading.ML";
     5.8 +
     5.9 +
    5.10  (** ML system and platform related **)
    5.11  
    5.12  (* String compatibility *)
     6.1 --- a/src/Pure/ML-Systems/smlnj.ML	Mon Jul 23 13:50:31 2007 +0200
     6.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Mon Jul 23 14:06:11 2007 +0200
     6.3 @@ -4,6 +4,8 @@
     6.4  Compatibility file for Standard ML of New Jersey 110 or later.
     6.5  *)
     6.6  
     6.7 +use "ML-Systems/no_multithreading.ML";
     6.8 +
     6.9  
    6.10  (** ML system related **)
    6.11  
     7.1 --- a/src/Pure/Thy/thm_database.ML	Mon Jul 23 13:50:31 2007 +0200
     7.2 +++ b/src/Pure/Thy/thm_database.ML	Mon Jul 23 14:06:11 2007 +0200
     7.3 @@ -51,14 +51,15 @@
     7.4  fun ml_store_thm (name, thm) =
     7.5    let val thm' = store_thm (name, thm) in
     7.6      if warn_ml name then ()
     7.7 -    else (qed_thms := [thm'];
     7.8 -      use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);"))
     7.9 +    else CRITICAL (fn () => (qed_thms := [thm'];
    7.10 +      use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);")))
    7.11    end;
    7.12  
    7.13  fun ml_store_thms (name, thms) =
    7.14    let val thms' = store_thms (name, thms) in
    7.15      if warn_ml name then ()
    7.16 -    else (qed_thms := thms'; use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;"))
    7.17 +    else CRITICAL (fn () => (qed_thms := thms';
    7.18 +      use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;")))
    7.19    end;
    7.20  
    7.21