From 4af41a12a0e7e6b17d25a71568641bd03d5e1f94 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 14 Feb 2018 06:57:40 +0100 Subject: [located] More work towards using CAst.t We continue with the work of #402 and #6745 and update most of the remaining parts of the AST: - module declarations - intro patterns - top-level sentences Now, parsed documents should be full annotated by `CAst` nodes. --- stm/stm.ml | 8 ++++---- stm/stm.mli | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index b3da97c6e..b1cecc6d1 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1084,7 +1084,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t | VernacShow ShowScript -> ShowScript.show_script (); st (** XX we are ignoring control here *) | _ -> stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); - try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (Loc.tag ?loc expr) + try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (CAst.make ?loc expr) with e -> let e = CErrors.push e in Exninfo.iraise Hooks.(call_process_error_once e) @@ -2992,7 +2992,7 @@ let parse_sentence ~doc sid pa = try match Pcoq.Gram.entry_parse Pcoq.main_entry pa with | None -> raise End_of_input - | Some (loc, cmd) -> Loc.tag ~loc cmd + | Some (loc, cmd) -> CAst.make ~loc cmd with e when CErrors.noncritical e -> let (e, info) = CErrors.push e in Exninfo.iraise (e, info)) @@ -3033,7 +3033,7 @@ let compute_indentation ?loc sid = Option.cata (fun loc -> eff_indent, len ) (0, 0) loc -let add ~doc ~ontop ?newtip verb (loc, ast) = +let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } = let cur_tip = VCS.cur_tip () in if not (Stateid.equal ontop cur_tip) then user_err ?loc ~hdr:"Stm.add" @@ -3063,7 +3063,7 @@ let query ~doc ~at ~route s = else Reach.known_state ~cache:`Yes at; try while true do - let loc, ast = parse_sentence ~doc at s in + let { CAst.loc; v=ast } = parse_sentence ~doc at s in let indentation, strlen = compute_indentation ?loc at in CWarnings.set_current_loc loc; let clas = Vernac_classifier.classify_vernac ast in diff --git a/stm/stm.mli b/stm/stm.mli index f967c9815..a8eb10fb3 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -80,7 +80,7 @@ val new_doc : stm_init_options -> doc * Stateid.t (* [parse_sentence sid pa] Reads a sentence from [pa] with parsing state [sid] Returns [End_of_input] if the stream ends *) val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable -> - Vernacexpr.vernac_control Loc.located + Vernacexpr.vernac_control CAst.t (* Reminder: A parsable [pa] is constructed using [Pcoq.Gram.coq_parsable stream], where [stream : char Stream.t]. *) @@ -94,7 +94,7 @@ exception End_of_input If [newtip] is provided, then the returned state id is guaranteed to be [newtip] *) val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> - bool -> Vernacexpr.vernac_control Loc.located -> + bool -> Vernacexpr.vernac_control CAst.t -> doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] (* [query at ?report_with cmd] Executes [cmd] at a given state [at], -- cgit v1.2.3