diff options
| author | ppedrot | 2012-05-13 01:05:45 +0000 |
|---|---|---|
| committer | ppedrot | 2012-05-13 01:05:45 +0000 |
| commit | 8d91c8808f2655be188615f420d345a00e3a7bdc (patch) | |
| tree | ac65f228847630af4c72774adebb59e3f20a5395 /ide/wg_Command.ml | |
| parent | 8ca5c2456d8e2a614a48b6d739f133fbcf97f1d1 (diff) | |
Heavily rewritten the coqtop management process of coqide. The coqtop
object is now responsible for restarting itself, and handles unexpected
crashes. Fixes a lot of errors in file descriptor management, but may
introduce lurking deadlocks and nasty bugs waiting to be discovered.
Only (quickly) tested under Linux, any callbacks from Windows are welcome.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15314 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/wg_Command.ml')
| -rw-r--r-- | ide/wg_Command.ml | 19 |
1 files changed, 8 insertions, 11 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index d52be74cb7..e15e1960b9 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -111,17 +111,14 @@ object(self) if String.get com (String.length com - 1) = '.' then com ^ " " else com ^ " " ^ entry#text ^" . " in - try - result#buffer#set_text - (match Coq.interp !coqtop ~raw:true phrase with - | Interface.Fail (l,str) -> - ("Error while interpreting "^phrase^":\n"^str) - | Interface.Good results -> - ("Result for command " ^ phrase ^ ":\n" ^ results)) - with e -> - let s = Printexc.to_string e in - assert (Glib.Utf8.validate s); - result#buffer#set_text s + Coq.try_grab coqtop begin fun handle -> + result#buffer#set_text + (match Coq.interp handle ~raw:true phrase with + | Interface.Fail (l,str) -> + ("Error while interpreting "^phrase^":\n"^str) + | Interface.Good results -> + ("Result for command " ^ phrase ^ ":\n" ^ results)) + end ignore in ignore (combo#entry#connect#activate ~callback:(on_activate callback)); ignore (ok_b#connect#clicked ~callback:(on_activate callback)); |