Skip to content

Commit

Permalink
Make possible fix for uninterruptibility problem
Browse files Browse the repository at this point in the history 
Isabelle's treatment of interrupts is not appropriate for use of a
"console" application like HOL.  I think I've made a reasonable fix to
the way interrupts are stored and restored.
  • Loading branch information
@mn200
mn200 committed Oct 3, 2018
1 parent b42a4b7 commit ef4c7ca
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/portableML/poly/Thread_Attributes.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -90,8 +90,8 @@ fun safe_interrupts (Attributes w) =

fun with_attributes new_atts e =
let
val atts1 = safe_interrupts (get_attributes ());
val atts2 = safe_interrupts new_atts;
val atts1 = get_attributes ()
val atts2 = safe_interrupts new_atts
in
if atts1 = atts2 then e atts1
else
Expand Down

1 comment on commit ef4c7ca

@binghe
Copy link
Member

@binghe binghe commented on ef4c7ca Oct 12, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hi, I confirm the uninterruptibility problem has been fixed by this commit, as I didn't meet this issue again, i.e. I can always interrupt PROVE_TAC and METIS_TAC immediately. Thanks for your fixes.

Please sign in to comment.