+ let ty,_ = CTC.type_of_aux' metasenv context term ugraph in
+ let t_and_ty = Cic.Cast (term,ty) in
+ guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
+ [], parsed_text_length
+(* | TA.Abort _ ->
+ let rec go_back () =
+ let status = script#status.proof_status in
+ match status with
+ | No_proof -> ()
+ | _ -> script#retract ();go_back()
+ in
+ [], parsed_text_length, Some go_back
+ | TA.Redo (_, Some i) -> [], parsed_text_length,
+ Some (fun () -> for j = 1 to i do advance () done)
+ | TA.Redo (_, None) -> [], parsed_text_length,
+ Some (fun () -> advance ())
+ | TA.Undo (_, Some i) -> [], parsed_text_length,
+ Some (fun () -> for j = 1 to i do script#retract () done)
+ | TA.Undo (_, None) -> [], parsed_text_length,
+ Some (fun () -> script#retract ()) *)
+ (* TODO *)
+ | TA.Quit _ -> failwith "not implemented"
+ | TA.Print (_,kind) -> failwith "not implemented"
+ | TA.Search_pat (_, search_kind, str) -> failwith "not implemented"
+ | TA.Search_term (_, search_kind, term) -> failwith "not implemented"
+
+
+let eval_executable guistuff status user_goal parsed_text script ex =
+ let module TA = GrafiteAst in
+ let module TAPp = GrafiteAstPp in
+ let module MD = MatitaDisambiguator in
+ let module ML = MatitacleanLib in
+ let parsed_text_length = String.length parsed_text in
+ match ex with
+ | TA.Command (loc, _) | TA.Tactical (loc, _) ->
+ (try
+ (match ML.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
+ | None -> ()
+ | Some u ->
+ if not (ML.is_empty u) then
+ match
+ guistuff.ask_confirmation
+ ~title:"Baseuri redefinition"
+ ~message:(
+ "Baseuri " ^ u ^ " already exists.\n" ^
+ "Do you want to redefine the corresponding "^
+ "part of the library?")
+ with
+ | `YES -> MatitacleanLib.clean_baseuris [u]
+ | `NO -> ()
+ | `CANCEL -> raise MatitaTypes.Cancel);
+ eval_with_engine
+ guistuff status user_goal parsed_text (TA.Executable (loc, ex))
+ with MatitaTypes.Cancel -> [], 0)
+ | TA.Macro (_,mac) ->
+ eval_macro guistuff status parsed_text script mac
+
+let rec eval_statement guistuff status user_goal script s =
+ if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
+ let st = GrafiteParser.parse_statement (Stream.of_string s) in
+ let text_of_loc loc =
+ let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in
+ let parsed_text = safe_substring s 0 parsed_text_length in
+ parsed_text, parsed_text_length
+ in
+ match st with
+ | GrafiteAst.Comment (loc,_)->
+ let parsed_text, parsed_text_length = text_of_loc loc in
+ let remain_len = String.length s - parsed_text_length in
+ let s = String.sub s parsed_text_length remain_len in
+ let s,len =
+ eval_statement guistuff status user_goal script s
+ in
+ (match s with
+ | (status, text) :: tl ->
+ ((status, parsed_text ^ text)::tl), (parsed_text_length + len)
+ | [] -> [], 0)
+ | GrafiteAst.Executable (loc, ex) ->
+ let parsed_text, parsed_text_length = text_of_loc loc in
+ eval_executable guistuff status user_goal parsed_text script ex
+
+let fresh_script_id =
+ let i = ref 0 in
+ fun () -> incr i; !i
+
+class script ~(view: GText.view)
+ ~(init: MatitaTypes.status)
+ ~(mathviewer: MatitaTypes.mathViewer)
+ ~set_star
+ ~ask_confirmation
+ ~urichooser
+ ~develcreator
+ () =
+let buffer = view#buffer in
+object (self)
+ val scriptId = fresh_script_id ()
+
+ val guistuff = {
+ mathviewer = mathviewer;
+ urichooser = urichooser;
+ ask_confirmation = ask_confirmation;
+ develcreator = develcreator;
+ filenamedata = (None, None)}
+
+ method private getFilename =
+ match guistuff.filenamedata with Some f,_ -> f | _ -> assert false
+
+ method private ppFilename =
+ match guistuff.filenamedata with
+ | Some f,_ -> f
+ | None,_ -> sprintf ".unnamed%d.ma" scriptId
+
+ initializer
+ ignore(GMain.Timeout.add ~ms:300000
+ ~callback:(fun _ -> self#_saveToBackuptFile ();true));
+ ignore(buffer#connect#modified_changed
+ (fun _ -> if buffer#modified then
+ set_star self#ppFilename true
+ else
+ set_star self#ppFilename false))
+
+ val mutable statements = []; (** executed statements *)
+ val mutable history = [ init ];
+ (** list of states before having executed statements. Head element of this
+ * list is the current state, last element is the state at the beginning of
+ * the script.
+ * Invariant: this list length is 1 + length of statements *)
+
+ (** goal as seen by the user (i.e. metano corresponding to current tab) *)
+ val mutable userGoal = ~-1
+
+ (** text mark and tag representing locked part of a script *)
+ val locked_mark =
+ buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
+ val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
+
+ method locked_mark = locked_mark
+
+ (* history can't be empty, the invariant above grant that it contains at
+ * least the init status *)
+ method status = match history with hd :: _ -> hd | _ -> assert false
+
+ method private _advance ?statement () =
+ let s = match statement with Some s -> s | None -> self#getFuture in
+ MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
+ let (entries, parsed_len) =
+ eval_statement guistuff self#status userGoal self s
+ in
+ let (new_statuses, new_statements) = List.split entries in
+(*
+prerr_endline "evalStatement returned";
+List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
+*)
+ history <- List.rev new_statuses @ history;
+ statements <- List.rev new_statements @ statements;
+ let start = buffer#get_iter_at_mark (`MARK locked_mark) in
+ let new_text = String.concat "" new_statements in
+ if new_text <> String.sub s 0 parsed_len then
+ begin
+(* prerr_endline ("new:" ^ new_text); *)
+(* prerr_endline ("s:" ^ String.sub s 0 parsed_len); *)
+ let stop = start#copy#forward_chars parsed_len in
+ buffer#delete ~start ~stop;
+ buffer#insert ~iter:start new_text;
+(* prerr_endline "AUTOMATICALLY MODIFIED!!!!!" *)