From e8a6467545c2814c9418889201e8be19c0cef201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Jan 2017 15:46:23 +0100 Subject: [location] Make location optional in Loc.located This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed and other times it printed nothing as the caller checked for `is_ghost` upstream. --- stm/stm.ml | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 38415c1dde..d41e0c94f7 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1111,7 +1111,7 @@ end (* }}} *) let hints = ref Aux_file.empty_aux_file let set_compilation_hints file = hints := Aux_file.load_aux_file_for file -let get_hint_ctx ?loc = +let get_hint_ctx loc = let s = Aux_file.get ?loc !hints "context_used" in match Str.split (Str.regexp ";") s with | ids :: _ -> @@ -2027,7 +2027,7 @@ let collect_proof keep cur hd brkind id = !Flags.compilation_mode = Flags.BuildVio -> assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch); (try - let name, hint = name ids, get_hint_ctx ?loc in + let name, hint = name ids, get_hint_ctx loc in let t, v = proof_no_using last in v.expr <- VernacProof(t, Some hint); `ASync (parent last,proof_using_ast last,accn,name,delegate name) @@ -2697,8 +2697,8 @@ let parse_sentence sid pa = 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 + | None -> raise End_of_input + | Some (loc, cmd) -> Loc.tag ~loc cmd with e when CErrors.noncritical e -> let (e, info) = CErrors.push e in Exninfo.iraise (e, info)) @@ -2723,7 +2723,7 @@ let ind_len_loc_of_id sid = Note, this could maybe improved by handling more cases in compute_indentation. *) -let compute_indentation sid loc = +let compute_indentation ?loc sid = Option.cata (fun loc -> let open Loc in (* The effective lenght is the lenght on the last line *) let len = loc.ep - loc.bp in @@ -2737,20 +2737,20 @@ let compute_indentation sid loc = eff_indent + prev_indent, len else eff_indent, len - + ) (0, 0) loc let add ~ontop ?newtip verb (loc, ast) = let cur_tip = VCS.cur_tip () in if not (Stateid.equal ontop cur_tip) then - user_err ~hdr:"Stm.add" + user_err ?loc ~hdr:"Stm.add" (str "Stm.add called for a different state (" ++ str (Stateid.to_string ontop) ++ str ") than the tip: " ++ str (Stateid.to_string cur_tip) ++ str "." ++ fnl () ++ str "This is not supported yet, sorry."); - let indentation, strlen = compute_indentation ontop loc in + let indentation, strlen = compute_indentation ?loc ontop in CWarnings.set_current_loc loc; (* XXX: Classifiy vernac should be moved inside process transaction *) let clas = classify_vernac ast in - let aast = { verbose = verb; indentation; strlen; loc = Some loc; expr = ast } in + let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in match process_transaction ?newtip aast clas with | `Ok -> VCS.cur_tip (), `NewTip | `Unfocus qed_id -> qed_id, `Unfocus (VCS.cur_tip ()) @@ -2768,10 +2768,10 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s = if Stateid.equal at Stateid.dummy then finish () else Reach.known_state ~cache:`Yes at; let loc, ast = parse_sentence at s in - let indentation, strlen = compute_indentation at loc in + let indentation, strlen = compute_indentation ?loc at in CWarnings.set_current_loc loc; let clas = classify_vernac ast in - let aast = { verbose = true; indentation; strlen; loc = Some loc; expr = ast } in + let aast = { verbose = true; indentation; strlen; loc; expr = ast } in match clas with | VtStm (w,_), _ -> ignore(process_transaction aast (VtStm (w,false), VtNow)) -- cgit v1.2.3