X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fmatita%2FmatitaTypes.ml;h=95618d142624e932493666da151773b8d9f412c5;hb=6912a028bef118d8e9d7c2847200510a9b055c6a;hp=5305ea463d66cec6a780a76c2cc6fefd14250362;hpb=ac813b7e251e4bac1a8a16befa628203775771ca;p=helm.git

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 5305ea463..95618d142 100644
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -43,6 +43,8 @@ let explain = function
   | CicTextualParser2.Parse_error (floc, msg) ->
       let (x, y) = CicAst.loc_of_floc floc in
       sprintf "parse error at character %d-%d: %s" x y msg
+  | CicEnvironment.Object_not_found uri ->
+      sprintf "object not found: %s" (UriManager.string_of_uri uri)
   | exn -> sprintf "Uncaught exception: %s" (Printexc.to_string exn)
 
 exception No_proof
@@ -73,16 +75,30 @@ class type console =
     method echo_error     : string -> unit
     method clear          : unit -> unit
     method wrap_exn       : 'a. (unit -> 'a) -> 'a option
+    method choose_uri     : string list -> string
+    method show : ?msg:string -> unit -> unit
   end
 
+type choose_uris_callback =
+  selection_mode:[`MULTIPLE|`SINGLE] ->
+  ?title:string -> ?msg:string -> ?nonvars_button:bool ->
+  string list ->
+    string list
+type choose_interp_callback = (string * string) list list -> int list
+
 class type disambiguator =
   object
-    method parserr: parserr
-    method setParserr: parserr -> unit
-
     method env: DisambiguateTypes.environment
     method setEnv: DisambiguateTypes.environment -> unit
 
+    method chooseUris: choose_uris_callback
+    method setChooseUris: choose_uris_callback -> unit
+
+    method chooseInterp: choose_interp_callback
+    method setChooseInterp: choose_interp_callback -> unit
+
+    method parserr: parserr
+
     method disambiguateTerm:
       ?context:Cic.context -> ?metasenv:Cic.metasenv ->
       ?env:DisambiguateTypes.environment ->
@@ -123,19 +139,40 @@ class type currentProof =
 
 type command_outcome = bool * bool
 
+type script_item =
+  [ `Tactic
+  | `Theorem
+  | `Qed of UriManager.uri
+  | `Def of UriManager.uri
+  | `Inductive of UriManager.uri
+  ]
+
 class type interpreter =
   object
-    method endOffset : int
     method evalAst : DisambiguateTypes.tactical -> command_outcome
     method evalPhrase : string -> command_outcome
 (*     method evalStream: char Stream.t -> command_outcome *)
-    method reset : unit
+    method endOffset : int
+    method lastItem: script_item option
+    method setState: [`Proof | `Command] -> unit
+    method setEvalAstCallback: (DisambiguateTypes.tactical -> unit) -> unit
   end
 
+type term_source =
+  [ `Ast of DisambiguateTypes.term
+  | `Cic of Cic.term * Cic.metasenv
+  | `String of string
+  ]
+
 class type mathViewer =
   object
-    method checkTerm: Cic.conjecture -> Cic.metasenv -> unit
-    method unload: unit -> unit
+    method checkTerm: term_source -> unit
+  end
+
+class type cicBrowser =
+  object
+    method loadUri: string -> unit
+    method loadTerm: term_source -> unit
   end
 
 type mml_of_cic_sequent =
@@ -152,13 +189,6 @@ type mml_of_cic_object =
 
 type namer = ProofEngineTypes.mk_fresh_name_type
 
-type choose_uris_callback =
-  selection_mode:[`MULTIPLE|`SINGLE] ->
-  ?title:string -> ?msg:string -> ?nonvars_button:bool ->
-  string list ->
-    string list
-type choose_interp_callback = (string * string) list list -> int list
-
 let mono_uris_callback ~selection_mode ?title ?msg ?nonvars_button _ =
   raise (Failure "ambiguous input")
 let mono_interp_callback _ = raise (Failure "ambiguous input")