1. buf fixed in eval_from_stream when first_statemente_only=true:

[helm.git] / matita / matitaScript.ml

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index 1a128fb1c753bfa58cd30c1631997e0742614b41..4c35019bca8308c408b8462be9255a2a68cab40d 100644 (file)
--- 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