+ [ new_status , (extra_text, ast) ], parsed_text_length
+ | _ ->
+ HLog.error
+ "The result of the urichooser should be only 1 uri, not:\n";
+ List.iter (
+ fun u -> HLog.error (UriManager.string_of_uri u ^ "\n")
+ ) selected;
+ assert false)
+ | TA.Check (_,term) ->
+ let metasenv = GrafiteTypes.get_proof_metasenv status in
+ let context = GrafiteTypes.get_proof_context status user_goal in
+ let interps =
+ MatitaDisambiguator.disambiguate_term ~dbd ~context ~metasenv
+ ~aliases:status.aliases ~universe:(Some status.multi_aliases) term
+ in
+ let _, metasenv , term, ugraph =
+ match interps with
+ | [x], _ -> x
+ | _ -> assert false
+ in
+ 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 unparsed_text parsed_text script
+ ex
+=
+ let module TAPp = GrafiteAstPp in
+ let module MD = MatitaDisambiguator in
+ let module ML = MatitaMisc in
+ match ex with
+ | TA.Command (loc, _) | TA.Tactical (loc, _, _) ->
+ (try
+ (match GrafiteMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
+ | None -> ()
+ | Some u ->
+ if not (GrafiteMisc.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 ->
+ let basedir = Helm_registry.get "matita.basedir" in
+ LibraryClean.clean_baseuris ~basedir [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 user_goal unparsed_text parsed_text script mac
+
+let rec eval_statement (buffer : GText.buffer) guistuff status user_goal
+ script statement
+=
+ let st, unparsed_text =
+ match statement with
+ | `Raw text ->
+ if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
+ GrafiteParser.parse_statement (Ulexing.from_utf8_string text), text
+ | `Ast (st, text) -> st, text
+ in
+ let text_of_loc loc =
+ let parsed_text_length = snd (HExtlib.loc_of_floc loc) in
+ let parsed_text = safe_substring unparsed_text 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 unparsed_text - parsed_text_length in
+ let s = String.sub unparsed_text parsed_text_length remain_len in
+ let s,len =
+ try
+ eval_statement buffer guistuff status user_goal script
+ (`Raw s)
+ with
+ HExtlib.Localized (floc, exn) ->
+ HExtlib.raise_localized_exception ~offset:parsed_text_length floc exn
+ | MatitaDisambiguator.DisambiguationError (offset,errorll) ->
+ raise
+ (MatitaDisambiguator.DisambiguationError
+ (offset+parsed_text_length, errorll))
+ in
+ (match s with
+ | (status, (text, ast)) :: tl ->
+ ((status, (parsed_text ^ text, ast))::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 unparsed_text parsed_text
+ script ex
+
+let fresh_script_id =
+ let i = ref 0 in
+ fun () -> incr i; !i
+
+class script ~(source_view: GSourceView.source_view)
+ ~(init: GrafiteTypes.status)
+ ~(mathviewer: MatitaTypes.mathViewer)
+ ~set_star
+ ~ask_confirmation
+ ~urichooser
+ ~develcreator
+ () =
+let buffer = source_view#buffer in
+let source_buffer = source_view#source_buffer in