# HG changeset patch # User wenzelm # Date 1185201901 -7200 # Node ID e1a792312472bbec89d23ff86b15bc1983d3630f # Parent 7afee4bf89e8ad1c57a73e4e5a5a19f5d0054bf6 marked some CRITICAL sections; diff -r 7afee4bf89e8 -r e1a792312472 src/Pure/General/source.ML --- a/src/Pure/General/source.ML Mon Jul 23 16:45:00 2007 +0200 +++ b/src/Pure/General/source.ML Mon Jul 23 16:45:01 2007 +0200 @@ -114,24 +114,26 @@ (* stream source *) -fun slurp_input instream = +fun slurp_input instream = CRITICAL (fn () => let fun slurp () = (case TextIO.canInput (instream, 1) handle IO.Io _ => NONE of NONE => [] | SOME 0 => [] | SOME _ => TextIO.input instream :: slurp ()); - in maps explode (slurp ()) end; + in maps explode (slurp ()) end); fun drain_stream instream outstream prompt () = let val input = slurp_input instream in if exists (fn c => c = "\n") input then (input, ()) else - (TextIO.output (outstream, Output.output prompt); - TextIO.flushOut outstream; - (case TextIO.inputLine instream of + (case + CRITICAL (fn () => + (TextIO.output (outstream, Output.output prompt); + TextIO.flushOut outstream; + TextIO.inputLine instream)) of SOME line => (input @ explode line, ()) - | NONE => (input, ()))) + | NONE => (input, ())) end; fun of_stream instream outstream = diff -r 7afee4bf89e8 -r e1a792312472 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Mon Jul 23 16:45:00 2007 +0200 +++ b/src/Pure/pure_thy.ML Mon Jul 23 16:45:01 2007 +0200 @@ -304,11 +304,11 @@ (* hiding -- affects current theory node only *) -fun hide_thms fully names thy = +fun hide_thms fully names thy = CRITICAL (fn () => let val r as ref {theorems = (space, thms), index} = get_theorems_ref thy; val space' = fold (NameSpace.hide fully) names space; - in r := {theorems = (space', thms), index = index}; thy end; + in r := {theorems = (space', thms), index = index}; thy end); (* fact specifications *) @@ -343,7 +343,7 @@ fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name); fun enter_thms _ _ app_att ("", thms) thy = app_att (thy, thms) |> swap - | enter_thms pre_name post_name app_att (bname, thms) thy = + | enter_thms pre_name post_name app_att (bname, thms) thy = CRITICAL (fn () => let val name = Sign.full_name thy bname; val (thy', thms') = apsnd (post_name name) (app_att (thy, pre_name name thms)); @@ -359,7 +359,7 @@ else warn_overwrite name); r := {theorems = (space', theorems'), index = index'}; (thms', thy') - end; + end); (* add_thms(s) *)