(** creates a statement AST for the Goal tactic, e.g. "goal 7" *)
let goal_ast n =
let module A = GrafiteAst in
- let loc = Disambiguate.dummy_floc in
+ let loc = DisambiguateTypes.dummy_floc in
A.Executable (loc, A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n))))
type guistuff = {
let new_aliases =
match ex with
| TA.Command (_, TA.Alias _)
- | TA.Command (_, TA.Include _) -> DisambiguateTypes.Environment.empty
+ | TA.Command (_, TA.Include _)
+ | TA.Command (_, TA.Interpretation _) ->
+ DisambiguateTypes.Environment.empty
| _ -> MatitaSync.alias_diff ~from:status new_status
in
(* we remove the defined object since we consider them "automatic aliases" *)
let initial_space,status,new_status_and_text_list_rev =
let module DTE = DisambiguateTypes.Environment in
let module UM = UriManager in
- DTE.fold (
+ DTE.fold_flatten (
fun k ((v,_) as value) (initial_space,status,acc) ->
let b =
try
let initial_space =
if initial_space = "" then "\n" else initial_space in
initial_space ^
- DisambiguatePp.pp_environment(DTE.add k value DTE.empty) in
+ DisambiguatePp.pp_environment(DTE.cons k value DTE.empty) in
let new_status =
- {status with aliases = DTE.add k value status.aliases}
+ {status with aliases = DTE.cons k value status.aliases}
in
"\n",new_status,((new_status, new_text)::acc)
) new_aliases (initial_space,status,[]) in
let aliases = MatitaMisc.get_proof_aliases status in
let interps = MD.disambiguate_term dbd context metasenv aliases term in
match interps with
- | [_,_,x,_] -> x
+ | [_,_,x,_], _ -> x
| _ -> assert false
let eval_macro guistuff status unparsed_text parsed_text script mac =
in
let _, metasenv , term, ugraph =
match interps with
- | [x] -> x
+ | [x], _ -> x
| _ -> assert false
in
let ty,_ = CTC.type_of_aux' metasenv context term ugraph in
method private ppFilename =
match guistuff.filenamedata with
- | Some f,_ -> f
+ | Some f,_ -> Filename.basename f
| None,_ -> sprintf ".unnamed%d.ma" scriptId
initializer
method loadFromFile f =
buffer#set_text (MatitaMisc.input_file f);
- self#goto_top;
+ self#reset_buffer;
buffer#set_modified false
method assignFileName file =
end
method private goto_top =
- MatitaSync.time_travel ~present:self#status ~past:init;
+ MatitaSync.time_travel ~present:self#status ~past:init
+
+ method private reset_buffer =
statements <- [];
history <- [ init ];
userGoal <- ~-1;
+ self#notify;
buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter
method reset () =
- self#goto_top;
+ self#reset_buffer;
source_buffer#begin_not_undoable_action ();
buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter;
source_buffer#end_not_undoable_action ();
- self#notify;
buffer#set_modified false
-
+
method template () =
let template = MatitaMisc.input_file BuildTimeConf.script_template in
buffer#insert ~iter:(buffer#get_iter `START) template;
let getoldpos _ = buffer#get_iter_at_mark old_locked_mark in
let dispose_old_locked_mark () = buffer#delete_mark old_locked_mark in
match pos with
- | `Top -> dispose_old_locked_mark (); self#goto_top; self#notify
+ | `Top ->
+ dispose_old_locked_mark ();
+ self#goto_top;
+ self#reset_buffer;
+ self#notify
| `Bottom ->
(try
let rec dowhile () =