X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=c35fb9307232975b1b8409005aea93bcc1810562;hb=3ce38077e0b1e2a38ad513d3c108d7ef3c09bb7c;hp=49c3046b8eafeeaf74d0ccaa89635ac1df1289d4;hpb=c307d27343fe48aeeb2e1763a811f8122ac1c0df;p=helm.git diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 49c3046b8..c35fb9307 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -24,7 +24,7 @@ *) open Printf -open MatitaTypes +open GrafiteTypes module TA = GrafiteAst @@ -108,7 +108,9 @@ let eval_with_engine guistuff status user_goal parsed_text st = initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ] *) | _ -> initial_space,status,[] in let new_status = - MatitaEngine.eval_ast + GrafiteEngine.eval_ast + ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic + ~disambiguate_command:GrafiteDisambiguate.disambiguate_command ~include_paths:include_ ~do_heavy_checks:true new_status st in let new_aliases = @@ -126,13 +128,14 @@ let eval_with_engine guistuff status user_goal parsed_text st = let initial_space,status,new_status_and_text_list_rev = let module DTE = DisambiguateTypes.Environment in let module UM = UriManager in + let baseuri = GrafiteTypes.get_string_option new_status "baseuri" in List.fold_left ( fun (initial_space,status,acc) (k,((v,_) as value)) -> - let b = - try - let v = UM.strip_xpointer (UM.uri_of_string v) in - List.mem v new_status.objects - with UM.IllFormedUri _ -> false + let b = + try + UM.buri_of_uri (UM.uri_of_string v) = baseuri + with + UriManager.IllFormedUri _ -> false (* v is a description, not a URI *) in if b then initial_space,status,acc @@ -160,8 +163,8 @@ let eval_with_engine guistuff status user_goal parsed_text st = try eval_with_engine guistuff status user_goal parsed_text st with - | MatitaEngine.UnableToInclude what - | MatitaEngine.IncludedFileNotCompiled what as exc -> + | GrafiteEngine.UnableToInclude what + | GrafiteEngine.IncludedFileNotCompiled what as exc -> let compile_needed_and_go_on d = let target = what in let refresh_cb () = @@ -214,8 +217,8 @@ let eval_with_engine guistuff status user_goal parsed_text st = let disambiguate_macro_term term status user_goal = let module MD = MatitaDisambiguator in let dbd = LibraryDb.instance () in - let metasenv = MatitaTypes.get_proof_metasenv status in - let context = MatitaTypes.get_proof_context status user_goal in + let metasenv = GrafiteTypes.get_proof_metasenv status in + let context = GrafiteTypes.get_proof_context status user_goal in let interps = MD.disambiguate_term ~dbd ~context ~metasenv ~aliases:status.aliases ~universe:(Some status.multi_aliases) term in @@ -275,7 +278,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = [], parsed_text_length (* REAL macro *) | TA.Hint loc -> - let proof = MatitaTypes.get_current_proof status in + let proof = GrafiteTypes.get_current_proof status in let proof_status = proof, user_goal in let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in let selected = guistuff.urichooser l in @@ -289,7 +292,11 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = TA.Apply (loc, CicNotationPt.Uri (suri, None))), Some (TA.Dot loc)))) in - let new_status = MatitaEngine.eval_ast status ast in + let new_status = + GrafiteEngine.eval_ast + ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic + ~disambiguate_command:GrafiteDisambiguate.disambiguate_command + status ast in let extra_text = comment parsed_text ^ "\n" ^ TAPp.pp_statement ast @@ -303,8 +310,8 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = ) selected; assert false) | TA.Check (_,term) -> - let metasenv = MatitaTypes.get_proof_metasenv status in - let context = MatitaTypes.get_proof_context status user_goal in + 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 @@ -349,10 +356,10 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script match ex with | TA.Command (loc, _) | TA.Tactical (loc, _, _) -> (try - (match MatitaMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with + (match GrafiteMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with | None -> () | Some u -> - if not (MatitaMisc.is_empty u) then + if not (GrafiteMisc.is_empty u) then match guistuff.ask_confirmation ~title:"Baseuri redefinition" @@ -418,7 +425,7 @@ let fresh_script_id = fun () -> incr i; !i class script ~(source_view: GSourceView.source_view) - ~(init: MatitaTypes.status) + ~(init: GrafiteTypes.status) ~(mathviewer: MatitaTypes.mathViewer) ~set_star ~ask_confirmation @@ -589,7 +596,7 @@ object (self) val mutable observers = [] - method addObserver (o: MatitaTypes.status -> unit) = + method addObserver (o: GrafiteTypes.status -> unit) = observers <- o :: observers method private notify = @@ -736,10 +743,10 @@ object (self) | Intermediate _ -> assert false (* method proofStatus = MatitaTypes.get_proof_status self#status *) - method proofMetasenv = MatitaTypes.get_proof_metasenv self#status - method proofContext = MatitaTypes.get_proof_context self#status userGoal - method proofConclusion = MatitaTypes.get_proof_conclusion self#status userGoal - method stack = MatitaTypes.get_stack self#status + method proofMetasenv = GrafiteTypes.get_proof_metasenv self#status + method proofContext = GrafiteTypes.get_proof_context self#status userGoal + method proofConclusion= GrafiteTypes.get_proof_conclusion self#status userGoal + method stack = GrafiteTypes.get_stack self#status method setGoal n = userGoal <- n method goal = userGoal