src/Pure/ProofGeneral/proof_general_pgip.ML
changeset 32738 15bb09ca0378
parent 32144 183c1010ac14
child 32966 5b21661fe618
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -32,20 +32,20 @@
     1.4  (** print mode **)
     1.5  
     1.6  val proof_generalN = "ProofGeneral";
     1.7 -val pgmlsymbols_flag = ref true;
     1.8 +val pgmlsymbols_flag = Unsynchronized.ref true;
     1.9  
    1.10  
    1.11  (* assembling and issuing PGIP packets *)
    1.12  
    1.13 -val pgip_refid = ref NONE: string option ref;
    1.14 -val pgip_refseq = ref NONE: int option ref;
    1.15 +val pgip_refid = Unsynchronized.ref NONE: string option Unsynchronized.ref;
    1.16 +val pgip_refseq = Unsynchronized.ref NONE: int option Unsynchronized.ref;
    1.17  
    1.18  local
    1.19    val pgip_class  = "pg"
    1.20    val pgip_tag = "Isabelle/Isar"
    1.21 -  val pgip_id = ref ""
    1.22 -  val pgip_seq = ref 0
    1.23 -  fun pgip_serial () = inc pgip_seq
    1.24 +  val pgip_id = Unsynchronized.ref ""
    1.25 +  val pgip_seq = Unsynchronized.ref 0
    1.26 +  fun pgip_serial () = Unsynchronized.inc pgip_seq
    1.27  
    1.28    fun assemble_pgips pgips =
    1.29      Pgip { tag = SOME pgip_tag,
    1.30 @@ -65,7 +65,7 @@
    1.31  
    1.32  fun matching_pgip_id id = (id = ! pgip_id)
    1.33  
    1.34 -val output_xml_fn = ref Output.writeln_default
    1.35 +val output_xml_fn = Unsynchronized.ref Output.writeln_default
    1.36  fun output_xml s = ! output_xml_fn (XML.string_of s);
    1.37  
    1.38  val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
    1.39 @@ -280,7 +280,7 @@
    1.40  
    1.41  (* theorem dependeny output *)
    1.42  
    1.43 -val show_theorem_dependencies = ref false;
    1.44 +val show_theorem_dependencies = Unsynchronized.ref false;
    1.45  
    1.46  local
    1.47  
    1.48 @@ -368,13 +368,13 @@
    1.49  
    1.50  (* Preferences: tweak for PGIP interfaces *)
    1.51  
    1.52 -val preferences = ref Preferences.pure_preferences;
    1.53 +val preferences = Unsynchronized.ref Preferences.pure_preferences;
    1.54  
    1.55  fun add_preference cat pref =
    1.56 -  CRITICAL (fn () => change preferences (Preferences.add cat pref));
    1.57 +  CRITICAL (fn () => Unsynchronized.change preferences (Preferences.add cat pref));
    1.58  
    1.59  fun setup_preferences_tweak () =
    1.60 -  CRITICAL (fn () => change preferences
    1.61 +  CRITICAL (fn () => Unsynchronized.change preferences
    1.62     (Preferences.set_default ("show-question-marks", "false") #>
    1.63      Preferences.remove "show-question-marks" #>   (* we use markup, not ?s *)
    1.64      Preferences.remove "theorem-dependencies" #>  (* set internally *)
    1.65 @@ -471,7 +471,7 @@
    1.66  fun set_proverflag_pgmlsymbols b =
    1.67      (pgmlsymbols_flag := b;
    1.68        NAMED_CRITICAL "print_mode" (fn () =>
    1.69 -        change print_mode
    1.70 +        Unsynchronized.change print_mode
    1.71              (fn mode =>
    1.72                  remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else []))))
    1.73  
    1.74 @@ -677,7 +677,7 @@
    1.75     about this special status, but for now we just keep a local reference.
    1.76  *)
    1.77  
    1.78 -val currently_open_file = ref (NONE : pgipurl option)
    1.79 +val currently_open_file = Unsynchronized.ref (NONE : pgipurl option)
    1.80  
    1.81  fun get_currently_open_file () = ! currently_open_file;
    1.82  
    1.83 @@ -779,7 +779,7 @@
    1.84  *)
    1.85  
    1.86  local
    1.87 -    val current_working_dir = ref (NONE : string option)
    1.88 +    val current_working_dir = Unsynchronized.ref (NONE : string option)
    1.89  in
    1.90  fun changecwd_dir newdirpath =
    1.91     let
    1.92 @@ -1021,7 +1021,7 @@
    1.93  
    1.94  (* init *)
    1.95  
    1.96 -val initialized = ref false;
    1.97 +val initialized = Unsynchronized.ref false;
    1.98  
    1.99  fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
   1.100    | init_pgip true =
   1.101 @@ -1035,9 +1035,9 @@
   1.102           setup_present_hook ();
   1.103           init_pgip_session_id ();
   1.104           welcome ();
   1.105 -         set initialized);
   1.106 +         Unsynchronized.set initialized);
   1.107          sync_thy_loader ();
   1.108 -       change print_mode (update (op =) proof_generalN);
   1.109 +       Unsynchronized.change print_mode (update (op =) proof_generalN);
   1.110         pgip_toplevel tty_src);
   1.111  
   1.112  
   1.113 @@ -1045,7 +1045,7 @@
   1.114  (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
   1.115  
   1.116  local
   1.117 -    val pgip_output_channel = ref Output.writeln_default
   1.118 +    val pgip_output_channel = Unsynchronized.ref Output.writeln_default
   1.119  in
   1.120  
   1.121  (* Set recipient for PGIP results *)