- better error message on "unknown identifier"

- use newer (Andrea and Luca)'s box-based-pretty-printer

diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml
index 5abdec6e183935b77ca6a9925f8ec2de97ec3f0c..1b05e3c17fda7ecb24b2208f78b64d5eab204006 100644 (file)
--- 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)