src/HOL/Matrix/cplex/Cplex_tools.ML
changeset 32740 9dd0a2f83429
parent 32491 d5d8bea0cd94
child 35010 d6e492cea6e4
     1.1 --- a/src/HOL/Matrix/cplex/Cplex_tools.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/HOL/Matrix/cplex/Cplex_tools.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4  
     1.5  datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
     1.6  
     1.7 -val cplexsolver = ref SOLVER_DEFAULT;
     1.8 +val cplexsolver = Unsynchronized.ref SOLVER_DEFAULT;
     1.9  fun get_solver () = !cplexsolver;
    1.10  fun set_solver s = (cplexsolver := s);
    1.11  
    1.12 @@ -305,8 +305,8 @@
    1.13  fun load_cplexFile name =
    1.14      let
    1.15      val f = TextIO.openIn name
    1.16 -        val ignore_NL = ref true
    1.17 -    val rest = ref []
    1.18 +        val ignore_NL = Unsynchronized.ref true
    1.19 +    val rest = Unsynchronized.ref []
    1.20  
    1.21      fun is_symbol s c = (fst c) = TOKEN_SYMBOL andalso (to_upper (snd c)) = s
    1.22  
    1.23 @@ -612,7 +612,7 @@
    1.24  
    1.25      fun basic_write s = TextIO.output(f, s)
    1.26  
    1.27 -    val linebuf = ref ""
    1.28 +    val linebuf = Unsynchronized.ref ""
    1.29      fun buf_flushline s =
    1.30          (basic_write (!linebuf);
    1.31           basic_write "\n";
    1.32 @@ -860,7 +860,7 @@
    1.33  
    1.34      val f = TextIO.openIn name
    1.35  
    1.36 -    val rest = ref []
    1.37 +    val rest = Unsynchronized.ref []
    1.38  
    1.39      fun readToken_helper () =
    1.40          if length (!rest) > 0 then
    1.41 @@ -995,7 +995,7 @@
    1.42  
    1.43      val f = TextIO.openIn name
    1.44  
    1.45 -    val rest = ref []
    1.46 +    val rest = Unsynchronized.ref []
    1.47  
    1.48      fun readToken_helper () =
    1.49          if length (!rest) > 0 then