let no_options = StringMap.empty
type status = {
- aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
- proof_status: proof_status;
- options: options;
- coercions: CoercGraph.coercions;
- objects: (UriManager.uri * string) list;
- (** in-scope objects, with their paths *)
+ aliases : DisambiguateTypes.environment;
+ moo_content_rev : string list;
+ proof_status : proof_status;
+ options : options;
+ objects : (UriManager.uri * string) list;
+ notation_ids: CicNotation.notation_id list;
}
let dump_status status =
MatitaLog.message "status.aliases:\n";
MatitaLog.message
- (CicTextualParser2.EnvironmentP3.to_string status.aliases ^ "\n");
+ (DisambiguatePp.pp_environment status.aliases ^ "\n");
MatitaLog.message "status.proof_status:";
MatitaLog.message
(match status.proof_status with
in
MatitaLog.message (k ^ "::=" ^ v)) status.options;
MatitaLog.message "status.coercions\n";
- List.iter
- (fun (u1,u2,u3) -> MatitaLog.message
- ((UriManager.string_of_uri u1) ^
- (UriManager.string_of_uri u2) ^
- (UriManager.string_of_uri u3))) status.coercions;
MatitaLog.message "status.objects:\n";
List.iter
(fun (u,_) ->
with Failure _ ->
command_error (sprintf "Not an integer value \"%s\"" value))
in
- { status with options = StringMap.add name value status.options }
+ if StringMap.mem name status.options && name = "baseuri" then
+ command_error "Redefinition of 'baseuri' is forbidden."
+ else
+ { status with options = StringMap.add name value status.options }
(* subset of MatitaConsole.console methods needed by MatitaInterpreter *)
class type console =
| `Check of string (* term *)
| `Cic of Cic.term * Cic.metasenv
| `Dir of string (* "directory" in cic uris namespace *)
- | `Uri of string (* cic object uri *)
- | `Whelp of string * string list (* query and results *)
+ | `Uri of UriManager.uri (* cic object uri *)
+ | `Whelp of string * UriManager.uri list (* query and results *)
]
let string_of_entry = function
| `About `Us -> "about:us"
| `Check _ -> "check:"
| `Cic (_, _) -> "term:"
- | `Dir uri | `Uri uri -> uri
- | `Whelp (query, _) -> sprintf "whelp:%s" query
+ | `Dir uri -> uri
+ | `Uri uri -> UriManager.string_of_uri uri
+ | `Whelp (query, _) -> query
+
+let entry_of_string = function
+ | "about:blank" -> `About `Blank
+ | "about:proof" -> `About `Current_proof
+ | "about:us" -> `About `Us
+ | _ -> (* only about entries supported ATM *)
+ raise (Invalid_argument "entry_of_string")
class type mathViewer =
object
*)
method show_entry: ?reuse:bool -> mathViewer_entry -> unit
method show_uri_list:
- ?reuse:bool -> entry:mathViewer_entry -> string list -> unit
+ ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit
end