+(*
+ let new_lexicon_status,new_grafite_status =
+ MatitaEngine.eval_ast lexicon_status grafite_status ast in
+ let extra_text =
+ comment parsed_text ^ "\n" ^ pp_eager_statement_ast ast in
+ [ (new_grafite_status,new_lexicon_status), (extra_text, Some ast) ],
+ parsed_text_length
+*) assert false (* implementarla con una ricorsione *)
+ | _ ->
+ 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 grafite_status in
+ let context = GrafiteTypes.get_proof_context grafite_status user_goal in
+ let interps =
+ GrafiteDisambiguator.disambiguate_term ~dbd ~context ~metasenv
+ ~aliases:lexicon_status.LexiconEngine.aliases
+ ~universe:(Some lexicon_status.LexiconEngine.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 grafite_status = script#grafite_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 lexicon_status grafite_status user_goal unparsed_text parsed_text script ex
+=
+ let module TAPp = GrafiteAstPp in
+ let module MD = GrafiteDisambiguator in
+ let module ML = MatitaMisc in
+ match ex with
+ TA.Tactical (loc, _, _) ->
+ eval_with_engine
+ guistuff lexicon_status grafite_status user_goal parsed_text
+ (TA.Executable (loc, ex))
+ | TA.Command (loc, cmd) ->
+ (try
+ begin
+ match cmd with
+ | TA.Set (loc',"baseuri",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)
+ | _ -> ()
+ end;
+ eval_with_engine
+ guistuff lexicon_status grafite_status user_goal parsed_text
+ (TA.Executable (loc, ex))
+ with MatitaTypes.Cancel -> [], 0)
+ | TA.Macro (_,mac) ->
+ eval_macro guistuff lexicon_status grafite_status user_goal unparsed_text
+ parsed_text script mac
+
+let rec eval_statement (buffer : GText.buffer) guistuff lexicon_status
+ grafite_status user_goal script statement
+=
+ let (lexicon_status,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)
+ ~include_paths:(Helm_registry.get_list
+ Helm_registry.string "matita.includes")
+ lexicon_status, text
+ | `Ast (st, text) -> (lexicon_status, 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
+ | GrafiteParser.LNone loc ->
+ let parsed_text, parsed_text_length = text_of_loc loc in
+ [(grafite_status,lexicon_status),parsed_text],
+ parsed_text_length
+ | GrafiteParser.LSome (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 lexicon_status grafite_status user_goal
+ script (`Raw s)
+ with
+ HExtlib.Localized (floc, exn) ->
+ HExtlib.raise_localized_exception ~offset:parsed_text_length floc exn
+ | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
+ raise
+ (GrafiteDisambiguator.DisambiguationError
+ (offset+parsed_text_length, errorll))
+ in
+ (match s with
+ | (statuses,text)::tl ->
+ (statuses,parsed_text ^ text)::tl,parsed_text_length + len
+ | [] -> [], 0)
+ | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) ->
+ let parsed_text, parsed_text_length = text_of_loc loc in
+ eval_executable guistuff lexicon_status grafite_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)
+ ~(mathviewer: MatitaTypes.mathViewer)
+ ~set_star
+ ~ask_confirmation
+ ~urichooser
+ ~develcreator
+ () =
+let buffer = source_view#buffer in
+let source_buffer = source_view#source_buffer in
+let initial_statuses =
+ let include_paths =
+ Helm_registry.get_list Helm_registry.string "matita.includes" in
+ let lexicon_status =
+ CicNotation2.load_notation ~include_paths
+ BuildTimeConf.core_notation_script in
+ let grafite_status = GrafiteSync.init () in
+ grafite_status,lexicon_status
+in