X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ftestlibrary.ml;h=1b05e3c17fda7ecb24b2208f78b64d5eab204006;hb=c9995e146dc70bed25b9fe2913f3d5d31a4f9086;hp=5abdec6e183935b77ca6a9925f8ec2de97ec3f0c;hpb=fe1e7e151af9690f312259a4c1c969a1388bee5f;p=helm.git

diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml
index 5abdec6e1..1b05e3c17 100644
--- a/helm/gTopLevel/testlibrary.ml
+++ b/helm/gTopLevel/testlibrary.ml
@@ -20,7 +20,7 @@ module DisambiguateCallbacks =
      List.filter !uri_predicate choices
 
   let interactive_interpretation_choice _ = raise Multiple_interpretations
-  let input_or_locate_uri ~title = fail "Unknown identifier"
+  let input_or_locate_uri ~title = fail ("Unknown identifier: " ^ title)
  end
 
 module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)
@@ -38,9 +38,12 @@ let test_uri uri =
     let (ast, _) =
       Acic2Ast.ast_of_acic ids_to_inner_sorts ids_to_uris annterm
     in
-    debug_print ("ast: " ^ CicAstPp.pp_term ast);
+    let new_pp = BoxPp.pp_term ast in
+    debug_print ("ast:\n" ^ new_pp);
+    let new_ast = CicTextualParser2.parse_term (Stream.of_string new_pp) in
+    debug_print ("new_ast:\n" ^ CicAstPp.pp_term ast);
     let (_, _, term) =
-      Disambiguate'.disambiguate_term mqi_handle [] [] ast
+      Disambiguate'.disambiguate_term mqi_handle [] [] new_ast
         DisambiguateTypes.Environment.empty
     in
     debug_print ("term: " ^ CicPp.ppterm term)