!(Lazy.force basedir));
Quiet
| TacticAst.Command (TacticAst.Check term) ->
- let (_, _, term,ugraph) =
+ let (_, metasenv, term,ugraph) =
MatitaCicMisc.disambiguate ~disambiguator ~currentProof term
in
- let (context, metasenv) =
+ let (context, _) =
MatitaCicMisc.get_context_and_metasenv currentProof
in
(* this is the Eval Compute
(* TASSI: here ugraph1 is unused.... FIXME *)
let expr = Cic.Cast (term, ty) in
(match mathViewer with
- | Some v -> v#checkTerm (`Cic expr)
+ | Some v -> v#checkTerm (`Cic (expr, metasenv))
| _ -> ());
Quiet
| TacticAst.Command (TacticAst.Search_pat (search_kind, pat)) ->
Tactics.replace ~what:(self#disambiguate what)
~with_what:(self#disambiguate with_what)
| TacticAst.Auto -> Tactics.auto_new ~dbd
+ | TacticAst.Hint ->
+ let l = List.map fst
+ (MetadataQuery.experimental_hint ~dbd
+ (currentProof#proof#proof,currentProof#proof#goal))
+ in
+ let u = console#choose_uri l in
+ Tactics.apply (CicUtil.term_of_uri u)
| TacticAst.Change (what, with_what, _) ->
let what = self#disambiguate what in
let with_what = self#disambiguate with_what in
| `Proof -> (state <- proofState)
| `Command -> (state <- commandState)
+ method endOffset = state#endOffset
+
method private updateState = function
| New_state Command -> (state <- commandState)
| New_state Proof -> (state <- proofState)