diff options
| author | Emilio Jesus Gallego Arias | 2017-02-16 14:14:34 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-12 16:18:08 +0200 |
| commit | 3a7d9fcafedc4987d0748a8717b2b012a779de39 (patch) | |
| tree | 59bded0fc995c7a9137f909832592a9c8ee8807f /ide/ide_slave.ml | |
| parent | b209cea412a9541fd1c434dde36ea6eb1e256a33 (diff) | |
[stm] Remove edit_id.
We remove `edit_id` from the STM. In PIDE they serve a different
purpose, however in Coq they were of limited utility and required many
special cases all around the code.
Indeed, parsing is not an asynchronous operation in Coq, thus having
feedback about parsing didn't make much sense. All clients indeed
ignore such feedback and handle parsing in a synchronous way.
XML protocol clients are unaffected, they rely on the instead on the
Fail value.
This commit supersedes PR#203.
Diffstat (limited to 'ide/ide_slave.ml')
| -rw-r--r-- | ide/ide_slave.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 8cadf1a263..2d2b54678f 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -95,7 +95,7 @@ let ide_cmd_checks (loc,ast) = (** Interpretation (cf. [Ide_intf.interp]) *) let add ((s,eid),(sid,verbose)) = - let newid, rc = Stm.add ~ontop:sid verbose ~check:ide_cmd_checks eid s in + let newid, rc = Stm.add ~ontop:sid verbose ~check:ide_cmd_checks s in let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in (* TODO: the "" parameter is a leftover of the times the protocol * used to include stderr/stdout output. @@ -379,7 +379,7 @@ let init = let initial_id, _ = if not (is_in_load_paths (physical_path_of_string dir)) then Stm.add false ~ontop:(Stm.get_current_state ()) - 0 (Printf.sprintf "Add LoadPath \"%s\". " dir) + (Printf.sprintf "Add LoadPath \"%s\". " dir) else Stm.get_current_state (), `NewTip in if Filename.check_suffix file ".v" then Stm.set_compilation_hints file; |