guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], "", parsed_text_length
| TA.WHint (loc, term) ->
- let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in
+ let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term, []),0) in
let l = List.map fst (MQ.experimental_hint ~dbd s) in
let entry = `Whelp (pp_macro mac, l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
let t_and_ty = Cic.Cast (term,ty) in
guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
[], "", parsed_text_length
- | TA.Inline (_,suri) ->
+ | TA.Inline (_,style,suri,prefix) ->
let dbd = LibraryDb.instance () in
let uris =
let sql_pat =
(fun uri ->
prerr_endline ("Stampo " ^ UriManager.string_of_uri uri);
try
- ObjPp.obj_to_string 80
+ ObjPp.obj_to_string 78 style prefix (* FG: mi pare meglio 78 *)
(fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
with
- _ (* BRRRRRRRRR *) -> "ERRORE IN STAMPA DI " ^ UriManager.string_of_uri uri
+ | e (* BRRRRRRRRR *) ->
+ Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n"
+ (UriManager.string_of_uri uri) (Printexc.to_string e)
) sorted_uris_without_xpointer)
in
[],declarative,String.length parsed_text
with
| Margin -> self#notify
| Not_found -> assert false
+ | Invalid_argument "Array.make" -> HLog.error "The script is too big!\n"
| exc -> self#notify; raise exc
method retract () =
self#notify
with
| Margin -> self#notify
+ | Invalid_argument "Array.make" -> HLog.error "The script is too big!\n"
| exc -> self#notify; raise exc
method private getFuture =
set_star (Filename.basename self#ppFilename) false
method goto (pos: [`Top | `Bottom | `Cursor]) () =
+ try
let old_locked_mark =
`MARK
(buffer#create_mark ~name:"old_locked_mark"
| Margin -> dispose_remember (); dispose_old_locked_mark (); self#notify
| exc -> dispose_remember (); dispose_old_locked_mark ();
self#notify; raise exc)
-
+ with Invalid_argument "Array.make" ->
+ HLog.error "The script is too big!\n"
+
method onGoingProof () =
match self#grafite_status.proof_status with
| No_proof | Proof _ -> false
| HExtlib.Localized _
| CicNotationParser.Parse_error _ -> false
| Margin | End_of_file -> true
+ | Invalid_argument "Array.make" -> false
(* debug *)
method dump () =