X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaScript.ml;h=4c35019bca8308c408b8462be9255a2a68cab40d;hb=cb18dbb4e91bd392afa8552bf5f56b7a38dc669a;hp=1a128fb1c753bfa58cd30c1631997e0742614b41;hpb=06e2976ca4ef6bdfe14beba14ba538a2479c51a8;p=helm.git diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index 1a128fb1c..4c35019bc 100644 --- a/matita/matitaScript.ml +++ b/matita/matitaScript.ml @@ -234,7 +234,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status 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; @@ -331,7 +331,9 @@ prerr_endline ("Stampo " ^ UriManager.string_of_uri uri); 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