diff options
| -rw-r--r-- | dev/doc/changes.txt | 17 | ||||
| -rw-r--r-- | ide/ide_slave.ml | 27 | ||||
| -rw-r--r-- | stm/stm.ml | 130 | ||||
| -rw-r--r-- | stm/stm.mli | 41 |
4 files changed, 131 insertions, 84 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index af077bbb4..30edea7f2 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -139,6 +139,23 @@ document type". This allows for a more uniform handling of printing module Tag +** Stm API ** + +- We have streamlined the `Stm` API, now `add` and `query` take a + `coq_parsable` instead a `string` so clients can have more control + over their input stream. As a consequence, their types have been + modified. + +- The main parsing entry point has also been moved to the + `Stm`. Parsing is considered a synchronous operation so it will + either succeed of emit an exception. + +- `Feedback` is now only emitted for asynchronous operations. As a + consequence, it always carries a valid stateid and the type has + changed to accommodate that. + +- A few unused hooks were removed due to cleanups, no clients known. + ========================================= = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 2d2b54678..889757764 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -86,16 +86,19 @@ let ide_cmd_checks (loc,ast) = if is_debug ast then user_error "Debug mode not available in the IDE"; if is_known_option ast then - Feedback.msg_warning (strbrk "Set this option from the IDE menu instead"); + Feedback.msg_warning ~loc (strbrk "Set this option from the IDE menu instead"); if Vernac.is_navigation_vernac ast || is_undo ast then - Feedback.msg_warning (strbrk "Use IDE navigation instead"); + Feedback.msg_warning ~loc (strbrk "Use IDE navigation instead"); if is_query ast then - Feedback.msg_warning (strbrk "Query commands should not be inserted in scripts") + Feedback.msg_warning ~loc (strbrk "Query commands should not be inserted in scripts") (** Interpretation (cf. [Ide_intf.interp]) *) let add ((s,eid),(sid,verbose)) = - let newid, rc = Stm.add ~ontop:sid verbose ~check:ide_cmd_checks s in + let pa = Pcoq.Gram.parsable (Stream.of_string s) in + let loc_ast = Stm.parse_sentence sid pa in + ide_cmd_checks loc_ast; + let newid, rc = Stm.add ~ontop:sid verbose loc_ast 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. @@ -122,7 +125,9 @@ let edit_at id = * as not to break the core protocol for this minor change, but it should * be removed in the next version of the protocol. *) -let query (s,id) = Stm.query ~at:id s; "" +let query (s,id) = + let pa = Pcoq.Gram.parsable (Stream.of_string s) in + Stm.query ~at:id pa; "" let annotate phrase = let (loc, ast) = @@ -370,17 +375,19 @@ let init = fun file -> if !initialized then anomaly (str "Already initialized") else begin + let init_sid = Stm.get_current_state () in initialized := true; match file with - | None -> Stm.get_current_state () + | None -> init_sid | Some file -> let dir = Filename.dirname file in let open Loadpath in let open CUnix in let initial_id, _ = - if not (is_in_load_paths (physical_path_of_string dir)) then - Stm.add false ~ontop:(Stm.get_current_state ()) - (Printf.sprintf "Add LoadPath \"%s\". " dir) - else Stm.get_current_state (), `NewTip in + if not (is_in_load_paths (physical_path_of_string dir)) then begin + let pa = Pcoq.Gram.parsable (Stream.of_string (Printf.sprintf "Add LoadPath \"%s\". " dir)) in + let loc_ast = Stm.parse_sentence init_sid pa in + Stm.add false ~ontop:init_sid loc_ast + end else init_sid, `NewTip in if Filename.check_suffix file ".v" then Stm.set_compilation_hints file; Stm.finish (); diff --git a/stm/stm.ml b/stm/stm.ml index f8d959f97..fb0a0514d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -93,49 +93,6 @@ let may_pierce_opaque = function | { expr = VernacExtend (("ExtractionInductive",_), _) } -> true | _ -> false -(* Wrapper for Vernac.parse_sentence to set the feedback id *) -let indentation_of_string s = - let len = String.length s in - let rec aux n i precise = - if i >= len then 0, precise, len - else - match s.[i] with - | ' ' | '\t' -> aux (succ n) (succ i) precise - | '\n' | '\r' -> aux 0 (succ i) true - | _ -> n, precise, len in - aux 0 0 false - -(* We must parse on top of a state id, it should be something like: - - - get parsing information for that state. - - feed the parsable / parser with the right parsing information. - - call the parser - - Now, the invariant in ensured by the callers, but this is a bit - problematic. -*) -let stm_parse ?(indlen_prev=fun() -> 0) s = - let indentation, precise, strlen = indentation_of_string s in - let indentation = - if precise then indentation else indlen_prev () + indentation in - let pa = Pcoq.Gram.parsable (Stream.of_string s) in - Flags.with_option Flags.we_are_parsing (fun () -> - try - match Pcoq.Gram.entry_parse Pcoq.main_entry pa with - | None -> raise (Invalid_argument "stm_parse") - | Some (loc, ast) -> indentation, strlen, loc, ast - with e when CErrors.noncritical e -> - let (e, info) = CErrors.push e in - (* This is the old error recovery strategy. *) - (* let loc = Loc.get_loc info in *) - (* feedback (?newtip || eid) (Message(Error, loc, msg)) *) - iraise (e, info)) - () - -let pr_open_cur_subgoals () = - try Printer.pr_open_subgoals () - with Proof_global.NoCurrentProof -> Pp.str "" - let update_global_env () = if Proof_global.there_are_pending_proofs () then Proof_global.update_global_env () @@ -2385,6 +2342,10 @@ let observe id = VCS.restore vcs; iraise e +let pr_open_cur_subgoals () = + try Printer.pr_open_subgoals () + with Proof_global.NoCurrentProof -> Pp.str "" + let finish ?(print_goals=false) () = let head = VCS.current_branch () in observe (VCS.get_branch_pos head); @@ -2706,26 +2667,80 @@ let get_ast id = let stop_worker n = Slaves.cancel_worker n +(* We must parse on top of a state id, it should be something like: + + - get parsing information for that state. + - feed the parsable / parser with the right parsing information. + - call the parser + + Now, the invariant in ensured by the callers, but this is a bit + problematic. +*) +exception End_of_input + +let parse_sentence sid pa = + (* XXX: Should this restore the previous state? + Using reach here to try to really get to the + proper state makes the error resilience code fail *) + (* Reach.known_state ~cache:`Yes sid; *) + let cur_tip = VCS.cur_tip () in + if not (Stateid.equal sid cur_tip) then + user_err ~hdr:"Stm.parse_sentence" + (str "Currently, the parsing api only supports parsing at the tip of the document."); + Flags.with_option Flags.we_are_parsing (fun () -> + try + match Pcoq.Gram.entry_parse Pcoq.main_entry pa with + | None -> raise End_of_input + | Some com -> com + with e when CErrors.noncritical e -> + let (e, info) = CErrors.push e in + iraise (e, info)) + () + (* You may need to know the len + indentation of previous command to compute * the indentation of the current one. * Eg. foo. bar. * Here bar is indented of the indentation of foo + its strlen (4) *) -let ind_len_of id = - if Stateid.equal id Stateid.initial then 0 - else match (VCS.visit id).step with - | `Cmd { ctac = true; cast = { indentation; strlen } } -> - indentation + strlen - | _ -> 0 - -let add ~ontop ?newtip ?(check=ignore) verb s = +let ind_len_loc_of_id sid = + if Stateid.equal sid Stateid.initial then None + else match (VCS.visit sid).step with + | `Cmd { ctac = true; cast = { indentation; strlen; loc } } -> + Some (indentation, strlen, loc) + | _ -> None + +(* the indentation logic works like this: if the beginning of the + command is different than the start we are in a new line, thus + indentation follows from the starting position. Otherwise, we use + the previous one plus the offset. + + Note, this could maybe improved by handling more cases in + compute_indentation. *) + +let compute_indentation sid loc = + let open Loc in + (* The effective lenght is the lenght on the last line *) + let len = loc.ep - loc.bp in + let prev_indent = match ind_len_loc_of_id sid with + | None -> 0 + | Some (i,l,p) -> i + l + in + (* Now if the line has not changed, the need to add the previous indent *) + let eff_indent = loc.bp - loc.bol_pos in + if loc.bol_pos = 0 then + eff_indent + prev_indent, len + else + eff_indent, len + + +let add ~ontop ?newtip verb (loc, ast) = let cur_tip = VCS.cur_tip () in if not (Stateid.equal ontop cur_tip) then - (* For now, arbitrary edits should be announced with edit_at *) - anomaly(str"Not yet implemented, the GUI should not try this"); - let indentation, strlen, loc, ast = - stm_parse ~indlen_prev:(fun () -> ind_len_of ontop) s in + user_err ~hdr:"Stm.add" + (str "You used Stm.add on a different state than the tip" ++ fnl () ++ + str "This is not supported yet, sorry."); + let indentation, strlen = compute_indentation ontop loc in CWarnings.set_current_loc loc; - check(loc,ast); + (* XXX: Classifiy vernac should be moved inside process transaction *) let clas = classify_vernac ast in let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in match process_transaction ?newtip ~tty:false aast clas with @@ -2744,7 +2759,8 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s = Future.purify (fun s -> if Stateid.equal at Stateid.dummy then finish () else Reach.known_state ~cache:`Yes at; - let indentation, strlen, loc, ast = stm_parse s in + let loc, ast = parse_sentence at s in + let indentation, strlen = compute_indentation at loc in CWarnings.set_current_loc loc; let clas = classify_vernac ast in let aast = { verbose = true; indentation; strlen; loc; expr = ast } in diff --git a/stm/stm.mli b/stm/stm.mli index d3e5dde39..a31e4289d 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -13,24 +13,31 @@ open Loc (** state-transaction-machine interface *) -(* [add ontop check vebose eid s] adds a new command [s] on the state [ontop]. - [check] is called on the AST. - The [ontop] parameter is just for asserting the GUI is on sync, but - will eventually call edit_at on the fly if needed. - The sentence [s] is parsed in the state [ontop]. - If [newtip] is provided, then the returned state id is guaranteed to be - [newtip] *) -val add : - ontop:Stateid.t -> ?newtip:Stateid.t -> - ?check:(vernac_expr located -> unit) -> - bool -> string -> - Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] - -(* parses and executes a command at a given state, throws away its side effects - but for the printings. Feedback is sent with report_with (defaults to dummy - state id) *) +(* [parse_sentence sid pa] Reads a sentence from [pa] with parsing + state [sid] Returns [End_of_input] if the stream ends *) +val parse_sentence : Stateid.t -> Pcoq.Gram.coq_parsable -> + Vernacexpr.vernac_expr Loc.located + +(* Reminder: A parsable [pa] is constructed using + [Pcoq.Gram.coq_parsable stream], where [stream : char Stream.t]. *) + +exception End_of_input + +(* [add ~ontop ?newtip verbose cmd] adds a new command [cmd] ontop of + the state [ontop]. + The [ontop] parameter just asserts that the GUI is on + sync, but it will eventually call edit_at on the fly if needed. + If [newtip] is provided, then the returned state id is guaranteed + to be [newtip] *) +val add : ontop:Stateid.t -> ?newtip:Stateid.t -> + bool -> (Loc.t * Vernacexpr.vernac_expr) -> + Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] + +(* [query at ?report_with cmd] Executes [cmd] at a given state [at], + throwing away side effects except messages. Feedback will + be sent with [report_with], which defaults to the dummy state id *) val query : - at:Stateid.t -> ?report_with:(Stateid.t * Feedback.route_id) -> string -> unit + at:Stateid.t -> ?report_with:(Stateid.t * Feedback.route_id) -> Pcoq.Gram.coq_parsable -> unit (* [edit_at id] is issued to change the editing zone. [`NewTip] is returned if the requested id is the new document tip hence the document portion following |