+ let (st,new_statements,new_unparsed),parsed_len =
+ let rec do_exc = function
+ | MatitaEngine.EnrichedWithStatus (e,_) -> do_exc e
+ | NCicTypeChecker.TypeCheckerFailure s -> raise (Generic_error (Lazy.force s))
+ | HExtlib.Localized (floc,e) ->
+ let x, y = HExtlib.loc_of_floc floc in
+ let pre = Netconversion.ustring_sub `Enc_utf8 0 x text in
+ let err = Netconversion.ustring_sub `Enc_utf8 x (y-x) text in
+ let post = Netconversion.ustring_sub `Enc_utf8 y
+ (Netconversion.ustring_length `Enc_utf8 text - y) text in
+ let _,title = MatitaExcPp.to_string e in
+ (* let title = "" in *)
+ let marked =
+ pre ^ "\005span class=\"error\" title=\"" ^ title ^ "\"\006" ^ err ^ "\005/span\006" ^ post in
+ let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false
+ () (html_of_matita marked) in
+ raise (Emphasized_error marked)
+ | Disambiguate.NoWellTypedInterpretation (floc,e) ->
+ let x, y = HExtlib.loc_of_floc floc in
+ let pre = Netconversion.ustring_sub `Enc_utf8 0 x text in
+ let err = Netconversion.ustring_sub `Enc_utf8 x (y-x) text in
+ let post = Netconversion.ustring_sub `Enc_utf8 y
+ (Netconversion.ustring_length `Enc_utf8 text - y) text in
+ (*let _,title = MatitaExcPp.to_string e in*)
+ (* let title = "" in *)
+ let marked =
+ pre ^ "\005span class=\"error\" title=\"" ^ e ^ "\"\006" ^ err ^ "\005/span\006" ^ post in
+ let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false
+ () (html_of_matita marked) in
+ raise (Emphasized_error marked)
+ | NCicRefiner.Uncertain m as exn ->
+ let floc, e = Lazy.force m in
+ let x, y = HExtlib.loc_of_floc floc in
+ let pre = Netconversion.ustring_sub `Enc_utf8 0 x text in
+ let err = Netconversion.ustring_sub `Enc_utf8 x (y-x) text in
+ let post = Netconversion.ustring_sub `Enc_utf8 y
+ (Netconversion.ustring_length `Enc_utf8 text - y) text in
+ (* let _,title = MatitaExcPp.to_string e in *)
+ (* let title = "" in *)
+ let marked =
+ pre ^ "\005span class=\"error\" title=\"" ^ e ^ "\"\006" ^ err ^ "\005/span\006" ^ post in
+ let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false
+ () (html_of_matita marked) in
+ raise (Emphasized_error marked)
+ | NTacStatus.Error (s,None) as e ->
+ prerr_endline
+ ("NTacStatus.Error " ^ (Lazy.force s)); raise e
+ | NTacStatus.Error (s,Some exc) as e ->
+ prerr_endline
+ ("NTacStatus.Error " ^ Lazy.force s ^ " -- " ^ (Printexc.to_string exc));
+ do_exc exc
+ | GrafiteDisambiguate.Ambiguous_input (loc,choices) ->
+ let x,y = HExtlib.loc_of_floc loc in
+ let choice_of_alias = function
+ | GrafiteAst.Ident_alias (_,uri) -> uri, None, uri
+ | GrafiteAst.Number_alias (None,desc)
+ | GrafiteAst.Symbol_alias (_,None,desc) -> "cic:/fakeuri.def(1)", Some desc, desc
+ | GrafiteAst.Number_alias (Some uri,desc)
+ | GrafiteAst.Symbol_alias (_,Some uri,desc) -> uri, Some desc, desc
+ in
+ let tag_of_choice (uri,title,desc) =
+ match title with
+ | None -> Printf.sprintf "<choice href=\"%s\">%s</choice>"
+ uri
+ (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () desc)
+ | Some t -> Printf.sprintf "<choice href=\"%s\" title=\"%s\">%s</choice>"
+ uri
+ (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () t)
+ (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () desc)
+ in
+ let strchoices =
+ String.concat "\n"
+ (List.map (fun x -> tag_of_choice (choice_of_alias x)) choices)
+ in
+ prerr_endline (Printf.sprintf
+ "@@@ Ambiguous input at (%d,%d). Possible choices:\n\n%s\n\n@@@ End."
+ x y strchoices);
+ (*
+ let pre = Netconversion.ustring_sub `Enc_utf8 0 x text in
+ let err = Netconversion.ustring_sub `Enc_utf8 x (y-x) text in
+ let post = Netconversion.ustring_sub `Enc_utf8 y
+ (Netconversion.ustring_length `Enc_utf8 text - y) text in
+ let title = "Disambiguation Error" in
+ (* let title = "" in *)
+ let marked =
+ pre ^ "\005span class=\"error\" title=\"" ^ title ^ "\"\006" ^ err ^ "\005/span\006" ^ post in
+ let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false
+ () (html_of_matita marked) in
+ *)
+ let strchoices = Printf.sprintf
+ "<ambiguity start=\"%d\" stop=\"%d\">%s</ambiguity>" x y strchoices
+ in raise (Disamb_error strchoices)
+ | GrafiteDisambiguate.Error l -> raise (Disamb_error (xml_of_disamb_error l))
+ (* | End_of_file -> ... *)
+ | e ->
+ (* prerr_endline ("matitadaemon *** Unhandled exception " ^ Printexc.to_string e); *)
+ prerr_endline ("matitadaemon *** Unhandled exception " ^ snd (MatitaExcPp.to_string e));
+ raise e
+ in
+
+ try
+ eval_statement !include_paths (*buffer*) status (`Raw text)
+ with e -> do_exc e
+ in
+ debug "BEGIN PRINTGRAMMAR";
+ (*prerr_endline (Print_grammar.ebnf_of_term status);*)
+ (*let kwds = String.concat ", " status#get_kwds in
+ debug ("keywords = " ^ kwds );*)
+ debug "END PRINTGRAMMAR";