From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 18 Feb 2004 14:25:35 +0000 (+0000)
Subject: - better error message on "unknown identifier"
X-Git-Tag: v0_0_4~147
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dbdc6e721c121e2686ef9c9a012b4eb962299f14;p=helm.git

- 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 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)