From: Stefano Zacchiroli 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)