From 04168c737e0916ebdbcdb1457f228bef670c657b Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 6 Dec 2011 13:51:48 +0000 Subject: [PATCH] Matitaweb: 1) Added disambiguation error diagnostics, with web GUI 2) Detached MultiPassDisambiguator (still waiting to purge the code, though) 3) Detached stand alone GUI (i.e. matita and matita.opt) --- matitaB/components/disambiguation/Makefile | 3 +- .../components/disambiguation/disambiguate.ml | 238 ++++++++++-------- .../disambiguation/disambiguate.mli | 34 +-- .../disambiguation/multiPassDisambiguator.ml | 9 +- .../grafite_engine/grafiteEngine.ml | 5 +- .../grafite_engine/nCicCoercDeclaration.ml | 2 +- .../ng_disambiguation/grafiteDisambiguate.ml | 67 +++-- .../ng_disambiguation/grafiteDisambiguate.mli | 14 +- .../ng_disambiguation/nCicDisambiguate.ml | 44 ++-- .../ng_disambiguation/nCicDisambiguate.mli | 11 +- matitaB/components/ng_tactics/nTacStatus.ml | 2 +- matitaB/matita/Makefile | 6 +- matitaB/matita/matitaExcPp.ml | 4 +- matitaB/matita/matitaInit.ml | 2 +- matitaB/matita/matitaScript.ml | 4 +- matitaB/matita/matitadaemon.ml | 48 +++- matitaB/matita/matitaweb.js | 207 +++++++++++++++ 17 files changed, 504 insertions(+), 196 deletions(-) diff --git a/matitaB/components/disambiguation/Makefile b/matitaB/components/disambiguation/Makefile index d01dd73df..5f632d949 100644 --- a/matitaB/components/disambiguation/Makefile +++ b/matitaB/components/disambiguation/Makefile @@ -1,8 +1,7 @@ PACKAGE = disambiguation INTERFACE_FILES = \ disambiguateTypes.mli \ - disambiguate.mli \ - multiPassDisambiguator.mli + disambiguate.mli IMPLEMENTATION_FILES = \ $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) diff --git a/matitaB/components/disambiguation/disambiguate.ml b/matitaB/components/disambiguation/disambiguate.ml index a65dd3e5f..e78ca54a3 100644 --- a/matitaB/components/disambiguation/disambiguate.ml +++ b/matitaB/components/disambiguation/disambiguate.ml @@ -31,11 +31,11 @@ open DisambiguateTypes module Ast = NotationPt +(* hard errors, spurious errors *) exception NoWellTypedInterpretation of - int * - ((Stdpp.location list * string * string) list * - (DisambiguateTypes.domain_item * string) list * - (Stdpp.location * string) Lazy.t * bool) list + ((Stdpp.location * string) list * + (Stdpp.location * string) list) + exception PathNotWellFormed (** raised when an environment is not enough informative to decide *) @@ -133,6 +133,17 @@ type ('term,'metasenv,'subst,'graph) test_result = | Ko of (Stdpp.location * string) Lazy.t | Uncertain of (Stdpp.location * string) Lazy.t +type ('alias,'ast_thing,'metasenv,'subst,'thing,'ugraph) disamb_result = + | Disamb_success of ('ast_thing * 'metasenv * 'subst * 'thing * 'ugraph) list + (* each element of this list is a list of partially instantiated asts, + * sharing the last instantiated node, together with the location of that + * node; each ast is associated with the actual instantiation of the node, + * the refinement error, and the location at which refinement fails *) + | Disamb_failure of + (* hard errors, spurious errors *) + (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list * + (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list + let resolve ~env ~universe ~mk_choice item interpr arg = (* let _ = (mk_choice : (GrafiteAst.alias_spec -> 'b DisambiguateTypes.codomain_item)) in *) @@ -299,11 +310,11 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function ) [] defs in defs_dom @ where_dom - | Ast.Ident (name, x) -> - let x = match x with + | Ast.Ident (name, _x) -> + (* let x = match x with | `Uri u -> Some u - | _ -> None - in + | _ -> None + in *) (try (* the next line can raise Not_found *) ignore(find_in_context name context); [] @@ -480,50 +491,59 @@ let pattern_split ctx = function ;; (* this function is used to get the children of a given node, together with - * their context + * their context and their location * contexts are expressed in the form of functions Ast -> Ast *) -(* split : ('term -> 'a) -> 'term -> (('term -> 'a) * 'term) list *) -let rec split ctx = function +(* split : location -> ('term -> 'a) -> 'term -> (('term -> 'a) * 'term * loc) list *) +let rec split loc ctx t = + let loc_of_attr oldloc = function + | `Loc l -> l + | _ -> oldloc + in + match t with | Ast.AttributedTerm (attr,t) -> - [(fun x -> ctx (Ast.AttributedTerm(attr,x))),t] - | Ast.Appl tl -> list_split (*split*) (fun ctx0 t0 -> [ctx0,t0]) (fun x -> ctx (Ast.Appl x)) [] tl + [(fun x -> ctx (Ast.AttributedTerm(attr,x))),t, loc_of_attr loc attr] + | Ast.Appl tl -> list_split (*split*) (fun ctx0 t0 -> [ctx0,t0,loc]) (fun x -> ctx (Ast.Appl x)) [] tl | Ast.Binder (k,((n,None) as n'),body) -> - [ (fun v -> ctx (Ast.Binder (k,n',v))),body] + [ (fun v -> ctx (Ast.Binder (k,n',v))),body, loc] | Ast.Binder (k,((n,Some ty) as n'),body) -> - [(fun v -> ctx (Ast.Binder (k,(n,Some v),body))), ty - ;(fun v -> ctx (Ast.Binder (k,n',v))),body] + [(fun v -> ctx (Ast.Binder (k,(n,Some v),body))), ty, loc + ;(fun v -> ctx (Ast.Binder (k,n',v))),body, loc] | Ast.Case (t,ity,outty,pl) -> let outty_split = match outty with | None -> [] | Some u -> [(fun x -> ctx (Ast.Case (t,ity,Some x,pl))),u] in - ((fun x -> ctx (Ast.Case (x,ity,outty,pl))),t):: + List.map (fun (a,b) -> a,b,loc) + (((fun x -> ctx (Ast.Case (x,ity,outty,pl))),t):: outty_split@list_split (fun ctx0 (p,x) -> ((fun y -> ctx0 (p,y)),x)::pattern_split (fun y -> ctx0 (y,x)) p) (fun x -> ctx (Ast.Case(t,ity,outty,x))) - [] pl - | Ast.Cast (u,v) -> [ (fun x -> ctx (Ast.Cast (x,v))),u - ; (fun x -> ctx (Ast.Cast (u,x))),v ] + [] pl) + | Ast.Cast (u,v) -> [ (fun x -> ctx (Ast.Cast (x,v))),u,loc + ; (fun x -> ctx (Ast.Cast (u,x))),v,loc ] | Ast.LetIn ((n,None) as n',u,v) -> - [ (fun x -> ctx (Ast.LetIn (n',x,v))), u - ; (fun x -> ctx (Ast.LetIn (n',u,x))), v ] + [ (fun x -> ctx (Ast.LetIn (n',x,v))), u,loc + ; (fun x -> ctx (Ast.LetIn (n',u,x))), v,loc ] | Ast.LetIn ((n,Some t) as n',u,v) -> - [ (fun x -> ctx (Ast.LetIn ((n,Some x),u,v))), t - ; (fun x -> ctx (Ast.LetIn (n',x,v))), u - ; (fun x -> ctx (Ast.LetIn (n',u,x))), v ] + [ (fun x -> ctx (Ast.LetIn ((n,Some x),u,v))), t,loc + ; (fun x -> ctx (Ast.LetIn (n',x,v))), u, loc + ; (fun x -> ctx (Ast.LetIn (n',u,x))), v, loc ] | Ast.LetRec (k,funs,where) -> (* we do not use where any more?? *) - list_split letrecaux_split (fun x -> ctx (Ast.LetRec(k,x,where))) [] funs + List.map (fun (a,b) -> a,b,loc) + (list_split letrecaux_split (fun x -> ctx (Ast.LetRec(k,x,where))) [] funs) | _ -> [] (* leaves *) ;; +type 'ast marked_ast = + (NotationPt.term -> 'ast) * NotationPt.term * Stdpp.location -(* top_split : 'a -> ((term -> 'a) * term) list - * returns all the possible top-level (ctx,t) for its input *) +(* top_split : 'a -> ((term -> 'a) * term * loc) list + * such that it returns all the possible top-level (ctx,t,dummy_loc) for its input *) let bfvisit ~pp_term top_split test t = let rec aux = function | [] -> None - | (ctx0,t0 as hd)::tl -> + | (ctx0,t0,loc as hd)::tl -> (* prerr_endline ("ok! length tl = " ^ string_of_int (List.length tl)); *) debug_print (lazy ("visiting t0 = " ^ pp_term t0)); if test t0 then (debug_print (lazy "t0 is ambiguous"); Some hd) @@ -534,7 +554,7 @@ let bfvisit ~pp_term top_split test t = List.iter (fun (ctx',t') -> prerr_endline ("-- subnode " ^ (pp_term t'))) t0'; aux (tl@t0')) *) - let t0' = split ctx0 t0 in + let t0' = split loc ctx0 t0 in aux (tl@t0') (* in aux [(fun x -> x),t] *) in aux (top_split t) @@ -542,22 +562,24 @@ let bfvisit ~pp_term top_split test t = let obj_split (o:Ast.term Ast.obj) = match o with | Ast.Inductive (ls,itl) -> - list_split var_split (fun x -> Ast.Inductive (x,itl)) [] ls@ - list_split ity_split (fun x -> Ast.Inductive (ls,x)) [] itl + List.map (fun (a,b) -> a,b,Stdpp.dummy_loc) + (list_split var_split (fun x -> Ast.Inductive (x,itl)) [] ls@ + list_split ity_split (fun x -> Ast.Inductive (ls,x)) [] itl) | Ast.Theorem (flav,n,ty,None,p) -> - [(fun x -> Ast.Theorem (flav,n,x,None,p)), ty] + [(fun x -> Ast.Theorem (flav,n,x,None,p)), ty, Stdpp.dummy_loc] | Ast.Theorem (flav,n,ty,(Some bo as bo'),p) -> - [(fun x -> Ast.Theorem (flav,n,x,bo',p)), ty - ;(fun x -> Ast.Theorem (flav,n,ty,Some x,p)), bo] + [(fun x -> Ast.Theorem (flav,n,x,bo',p)), ty, Stdpp.dummy_loc + ;(fun x -> Ast.Theorem (flav,n,ty,Some x,p)), bo, Stdpp.dummy_loc] | Ast.Record (ls,n,ty,fl) -> - list_split var_split (fun x -> Ast.Record (x,n,ty,fl)) [] ls@ - [(fun x -> Ast.Record (ls,n,x,fl)),ty]@ - list_split field_split (fun x -> Ast.Record (ls,n,ty,x)) [] fl + List.map (fun (a,b) -> a,b,Stdpp.dummy_loc) + (list_split var_split (fun x -> Ast.Record (x,n,ty,fl)) [] ls@ + [(fun x -> Ast.Record (ls,n,x,fl)),ty]@ + list_split field_split (fun x -> Ast.Record (ls,n,ty,x)) [] fl) ;; let bfvisit_obj = bfvisit obj_split;; -let bfvisit = bfvisit (fun t -> [(fun x -> x),t]) ;; +let bfvisit = bfvisit (fun t -> [(fun x -> x),t,Stdpp.dummy_loc]) ;; let domain_item_of_ast = function | Ast.Ident (id,_) -> DisambiguateTypes.Id id @@ -576,6 +598,10 @@ let ast_of_alias_spec t alias = match (t,alias) with | _ -> assert false ;; +(* returns an optional (loc*string): + * - None means success (the ast is refinable) + * - Some (loc,err) means refinement has failed with error err at location loc + *) let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~universe ~uri ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl t = try @@ -589,20 +615,25 @@ let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~universe ~use_coercions cic_thing expty ugraph ~localization_tbl in match (refine_profiler.HExtlib.profile foo ()) with | Ko x -> - let _,err = Lazy.force x in + let loc,err = Lazy.force x in debug_print (lazy ("test_interpr error: " ^ err)); - false - | _ -> true + Some (loc,err) + | _ -> None with (*| Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg)) | Invalid_choice loc_msg -> Ko loc_msg*) - | Invalid_choice _ -> false - | _ -> true + | Invalid_choice x -> + let loc,err = Lazy.force x in Some (loc,err) + | _ -> None ;; +exception Not_ambiguous;; + let rec disambiguate_list ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri ~interpretate_thing - ~refine_thing ~ugraph ~visit ~universe ~mk_localization_tbl ~pp_thing ~pp_term ts = + ~refine_thing ~ugraph ~visit ~universe ~mk_localization_tbl ~pp_thing ~pp_term + ts errors = + let disambiguate_list = disambiguate_list ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri ~interpretate_thing ~refine_thing ~ugraph ~visit ~universe @@ -633,15 +664,15 @@ let rec disambiguate_list let get_instances ctx t = try let choices = find_choices (domain_item_of_ast t) in - List.map (fun t0 -> ctx (ast_of_alias_spec t t0)) choices + List.map (fun t0 -> ctx (ast_of_alias_spec t t0), t0) choices with | Not_found -> [] in match ts with - | [] -> None - | t0 :: tl -> - debug_print (lazy ("disambiguate_list: t0 = " ^ pp_thing t0)); + | [] -> [], errors + | _ -> + (* debug_print (lazy ("disambiguate_list: t0 = " ^ pp_thing t0)); *) let is_ambiguous = function | Ast.Ident (_,`Ambiguous) | Ast.Num (_,None) @@ -655,34 +686,53 @@ let rec disambiguate_list | Ast.Symbol (sym,_) -> "SYM " ^ sym | _ -> "ERROR!" in - (* get first ambiguous subterm (or return disambiguated term) *) - match visit ~pp_term is_ambiguous t0 with - | None -> - debug_print (lazy ("visit -- not ambiguous node:\n" ^ pp_thing t0)); - Some (t0,tl) - | Some (ctx, t) -> - debug_print (lazy ("visit -- found ambiguous node: " ^ astpp t ^ - "\nin " ^ pp_thing (ctx t))); - (* get possible instantiations of t *) - let instances = get_instances ctx t in - debug_print (lazy "-- possible instances:"); - List.iter - (fun u0 -> debug_print (lazy ("-- instance: " ^ (pp_thing u0)))) instances; - (* perforate ambiguous subterms and test refinement *) - debug_print (lazy "-- survivors:"); - let survivors = List.filter test_interpr instances in - List.iter - (fun u0 -> debug_print (lazy ("-- survivor: " ^ (pp_thing u0)))) survivors; - disambiguate_list (survivors@tl) + let process_ast t0 = + (* get first ambiguous subterm (or return disambiguated term) *) + match visit ~pp_term is_ambiguous t0 with + | None -> +(* debug_print (lazy ("visit -- not ambiguous node:\n" ^ pp_thing + * t0));*) + (* Some (t0,tl), errors *) + raise Not_ambiguous + | Some (ctx, t, loc_t) -> + debug_print (lazy ("visit -- found ambiguous node: " ^ astpp t ^ + "\nin " ^ pp_thing (ctx t))); + (* get possible instantiations of t *) + let instances = get_instances ctx t in + debug_print (lazy "-- possible instances:"); +(* List.iter + (fun u0 -> debug_print (lazy ("-- instance: " ^ (pp_thing u0)))) +instances; *) + (* perforate ambiguous subterms and test refinement *) + let instances = List.map (fun (x,a) -> (x,Some a),test_interpr x) instances in + debug_print (lazy "-- survivors:"); + let survivors, defuncts = + List.partition (fun (_,o) -> o = None) instances in + survivors, (defuncts, loc_t) + + in + try + let ts', new_errors = List.split (List.map process_ast ts) in + let ts' = List.map (fun ((t,_),_) -> t) (List.flatten ts') in + let errors' = match new_errors with + | (_,l)::_ -> + let ne' = + List.map (fun (a,b) -> a, HExtlib.unopt b) + (List.flatten (List.map fst new_errors)) in + let ne' = List.map (fun ((x,a),(l,e)) -> x,a,l,e) ne' in + (ne',l)::errors + | _ -> errors + in disambiguate_list ts' errors' + with Not_ambiguous -> ts,errors ;; let disambiguate_thing ~context ~metasenv ~subst ~use_coercions - ~string_context_of_context - ~initial_ugraph:base_univ ~expty - ~mk_implicit ~description_of_alias ~fix_instance - ~aliases ~universe ~lookup_in_library - ~uri ~pp_thing ~pp_term ~domain_of_thing ~interpretate_thing ~refine_thing + ~string_context_of_context ~initial_ugraph:base_univ + ~expty ~mk_implicit ~description_of_alias + ~fix_instance ~aliases ~universe + ~lookup_in_library ~uri ~pp_thing ~pp_term + ~domain_of_thing ~interpretate_thing ~refine_thing ~visit ~mk_localization_tbl (thing_txt,thing_txt_prefix_len,thing) = @@ -692,15 +742,12 @@ let disambiguate_thing ~env ~universe ~uri ~interpretate_thing ~refine_thing ~ugraph:base_univ ~mk_localization_tbl in (* real function *) - let rec aux tl = - match disambiguate_list ~mk_localization_tbl ~context ~metasenv ~subst + let aux tl = + disambiguate_list ~mk_localization_tbl ~context ~metasenv ~subst ~interpretate_thing ~refine_thing ~ugraph:base_univ ~visit ~use_coercions ~expty ~uri ~env ~universe ~pp_thing - ~pp_term tl with - | None -> [] - | Some (t,tl') -> t::aux tl' + ~pp_term tl [] in - let refine t = let localization_tbl = mk_localization_tbl 503 in debug_print (lazy "before interpretate_thing"); @@ -717,26 +764,21 @@ let disambiguate_thing assert false | _ -> assert false in - if not (test_interpr thing) then - (debug_print (lazy ("preliminary test fail: " ^ pp_thing thing)); - raise (NoWellTypedInterpretation (0,[]))) - else - let res = aux [thing] in - let res = - HExtlib.filter_map (fun t -> - try Some (refine t) + match (test_interpr thing) with + | Some (loc,err) -> +(* debug_print (lazy ("preliminary test fail: " ^ pp_thing thing)); *) + Disamb_failure ([[thing,None,loc,err],loc],[]) + | None -> + let res,errors = aux [thing] in + let res = + HExtlib.filter_map (fun t -> + try Some (refine t) with _ -> - debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t)));None) res +(* debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t)));*) + None) res in - match res with - | [] -> raise (NoWellTypedInterpretation (0,[])) - (* XXX : the boolean seems not to play a role any longer *) - | [t] -> res,false - | _ -> res, true - (* let choices = List.map (fun (t,_,_,_,_) -> pp_thing t) res in - let user_choice = interactive_ast_choice choices in - [ List.nth res user_choice ], true - (* let pp_thing (t,_,_,_,_,_) = prerr_endline ("interpretation: " ^ (pp_thing t)) in - List.iter pp_thing res; res,true *) *) + (match res with + | [] -> Disamb_failure (errors,[]) + | _ -> Disamb_success res) ;; diff --git a/matitaB/components/disambiguation/disambiguate.mli b/matitaB/components/disambiguation/disambiguate.mli index 2e6677d72..ab347e164 100644 --- a/matitaB/components/disambiguation/disambiguate.mli +++ b/matitaB/components/disambiguation/disambiguate.mli @@ -25,20 +25,16 @@ (** {2 Disambiguation interface} *) -(* the integer is an offset to be added to each location *) -(* list of located error messages, each list is a tuple: - * - environment in string form - * - environment patch - * - location - * - error message - * - significancy of the error message, if false the error is likely to be - * useless for the final user ... *) +type ('alias,'ast_thing,'metasenv,'subst,'thing,'ugraph) disamb_result = + | Disamb_success of ('ast_thing * 'metasenv * 'subst * 'thing * 'ugraph) list + | Disamb_failure of + (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list * + (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list + exception NoWellTypedInterpretation of - int * - ((Stdpp.location list * string * string) list * - (DisambiguateTypes.domain_item * string) list * - (Stdpp.location * string) Lazy.t * - bool) list + ((Stdpp.location * string) list * + (Stdpp.location * string) list) + exception PathNotWellFormed type 'a disambiguator_input = string * int * 'a @@ -125,17 +121,21 @@ val disambiguate_thing: ('refined_thing, 'metasenv,'subst,'ugraph) test_result) -> visit:(pp_term:(NotationPt.term -> string) -> (NotationPt.term -> bool) -> 'ast_thing -> - ((NotationPt.term -> 'ast_thing) * NotationPt.term) option) -> + ((NotationPt.term -> 'ast_thing) * NotationPt.term * Stdpp.location) option) -> mk_localization_tbl:(int -> 'cichash) -> 'ast_thing disambiguator_input -> - ('ast_thing * 'metasenv * 'subst * 'refined_thing * 'ugraph) list * bool + (GrafiteAst.alias_spec,'ast_thing,'metasenv,'subst,'refined_thing,'ugraph) disamb_result + +type 'ast marked_ast = + (NotationPt.term -> 'ast) * NotationPt.term * Stdpp.location val bfvisit : pp_term:(NotationPt.term -> string) -> (NotationPt.term -> bool) -> - NotationPt.term -> ((NotationPt.term -> NotationPt.term) * NotationPt.term) option + NotationPt.term -> (NotationPt.term marked_ast) option val bfvisit_obj : pp_term:(NotationPt.term -> string) -> (NotationPt.term -> bool) -> - NotationPt.term NotationPt.obj -> ((NotationPt.term -> NotationPt.term NotationPt.obj) * NotationPt.term) option + NotationPt.term NotationPt.obj -> + ((NotationPt.term NotationPt.obj) marked_ast) option diff --git a/matitaB/components/disambiguation/multiPassDisambiguator.ml b/matitaB/components/disambiguation/multiPassDisambiguator.ml index 2edd1bd69..da0cee2d4 100644 --- a/matitaB/components/disambiguation/multiPassDisambiguator.ml +++ b/matitaB/components/disambiguation/multiPassDisambiguator.ml @@ -166,7 +166,7 @@ let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~visit ~f thing *) - try + match Disambiguate.disambiguate_thing ~context ~metasenv ~subst ~use_coercions:true ~string_context_of_context ~initial_ugraph ~expty ~mk_implicit ~description_of_alias ~fix_instance @@ -174,5 +174,8 @@ let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing ~visit ~mk_localization_tbl ~pp_term thing with - | Disambiguate.NoWellTypedInterpretation (offset,newerrors) -> - raise (DisambiguationError (offset, [newerrors])) + | Disambiguate.Disamb_success res -> res + | Disambiguate.Disamb_failure (herrors, serrors) -> + (* temporary *) + let offset = 0 in + raise (DisambiguationError (offset, newerrors)) diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml index 5ac28559d..202111485 100644 --- a/matitaB/components/grafite_engine/grafiteEngine.ml +++ b/matitaB/components/grafite_engine/grafiteEngine.ml @@ -604,7 +604,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = else nstatus with - | MultiPassDisambiguator.DisambiguationError _ + | GrafiteDisambiguate.Error _ | NCicTypeChecker.TypeCheckerFailure _ -> (*HLog.warn "error in generating projection/eliminator";*) status @@ -659,7 +659,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = status (name,t,cpos,arity) in let aliases = GrafiteDisambiguate.aliases_for_objs status nuris in eval_alias status (mode,aliases) - with MultiPassDisambiguator.DisambiguationError _-> + with GrafiteDisambiguate.Error _ -> HLog.warn ("error in generating coercion: "^name); status) status coercions @@ -830,6 +830,7 @@ let rec eval_executable ~include_paths opts status (text,prefix_len,ex) = List.fold_left (fun status tac -> let status = eval_ng_tac (text,prefix_len,tac) status in + prerr_endline "prima di subst_metasenv_and_fix_names"; subst_metasenv_and_fix_names status) status tacl in diff --git a/matitaB/components/grafite_engine/nCicCoercDeclaration.ml b/matitaB/components/grafite_engine/nCicCoercDeclaration.ml index cf3c127b9..52b074c4a 100644 --- a/matitaB/components/grafite_engine/nCicCoercDeclaration.ml +++ b/matitaB/components/grafite_engine/nCicCoercDeclaration.ml @@ -145,7 +145,7 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt = with | NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ - | MultiPassDisambiguator.DisambiguationError _ -> + | GrafiteDisambiguate.Error _ -> raise (GrafiteTypes.Command_error "bad source pattern")) | _ -> assert false in diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml index 544128bef..c39ac161d 100644 --- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml +++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml @@ -79,6 +79,18 @@ class virtual status uid = (* reports the first source of ambiguity and its possible interpretations *) exception Ambiguous_input of (Stdpp.location * GrafiteAst.alias_spec list) +(* reports disambiguation errors *) +exception Error of + (* location of a choice point *) + (Stdpp.location * + (* one possible choice (or no valid choice) *) + (GrafiteAst.alias_spec option * + (* list of asts together with the failing location and error msg *) + ((Stdpp.location * GrafiteAst.alias_spec) list * + Stdpp.location * string) list) + list) + list + let dump_aliases out msg status = out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:"); DisambiguateTypes.InterprEnv.iter (fun _ x -> out (GrafiteAstPp.pp_alias x)) @@ -306,9 +318,20 @@ let rec find_diffs l = find_diffs tls ;; +(* clusterize a list of errors according to the last chosen interpretation *) +let clusterize diff (eframe,loc0) = + let rec aux = function + | [] -> [] + | (_,choice,_,_ as x)::l0 -> + let matches,others = List.partition (fun (_,c,_,_) -> c = choice) l0 in + (choice,List.map (fun (a,_,l,e) -> diff a,l,e) (x::matches)) :: + aux others + in loc0, aux eframe + let disambiguate_nterm status expty context metasenv subst thing = - let choices, _ = NCicDisambiguate.disambiguate_term + let _,_,thing' = thing in + match NCicDisambiguate.disambiguate_term status ~aliases:status#disambiguate_db.interpr ~expty @@ -318,21 +341,21 @@ let disambiguate_nterm status expty context metasenv subst thing ~mk_implicit ~fix_instance ~description_of_alias:GrafiteAst.description_of_alias ~context ~metasenv ~subst thing - in - let _,_,thing' = thing in - match choices with - | [newast, metasenv, subst, cic] -> + with + | Disambiguate.Disamb_success [newast,metasenv,subst,cic,_] -> let diff = diff_term Stdpp.dummy_loc thing' newast in let status = add_to_interpr status diff in metasenv, subst, status, cic - | [] -> assert false - | _ -> + | Disambiguate.Disamb_success (_::_ as choices) -> let diffs = - List.map (fun (ast,_,_,_) -> + List.map (fun (ast,_,_,_,_) -> diff_term Stdpp.dummy_loc thing' ast) choices - in - raise (Ambiguous_input (find_diffs diffs)) + in + raise (Ambiguous_input (find_diffs diffs)) + | Disambiguate.Disamb_failure (l,_) -> + raise (Error (List.map (clusterize (diff_term Stdpp.dummy_loc thing')) l)) + | _ -> assert false ;; type pattern = @@ -397,7 +420,7 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj as obj') = NUri.uri_of_string (baseuri ^ "/" ^ name) in - let choices, _ = NCicDisambiguate.disambiguate_obj + match NCicDisambiguate.disambiguate_obj status ~lookup_in_library:(nlookup_in_library status) ~description_of_alias:GrafiteAst.description_of_alias @@ -406,20 +429,20 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj as obj') = ~aliases:status#disambiguate_db.interpr ~universe:(status#disambiguate_db.multi_aliases) obj' - in - match choices with - | [ast, _, _, cic] -> - let diff = diff_obj Stdpp.dummy_loc obj ast in - let status = add_to_interpr status diff - in - status, cic - | [] -> assert false - | _ -> + with + | Disambiguate.Disamb_success [newast,_,_,cic,_] -> + let diff = diff_obj Stdpp.dummy_loc obj newast in + let status = add_to_interpr status diff + in status, cic + | Disambiguate.Disamb_success (_::_ as choices) -> let diffs = - List.map (fun (ast,_,_,_) -> + List.map (fun (ast,_,_,_,_) -> diff_obj Stdpp.dummy_loc obj ast) choices in - raise (Ambiguous_input (find_diffs diffs)) + raise (Ambiguous_input (find_diffs diffs)) + | Disambiguate.Disamb_failure (l,_) -> + raise (Error (List.map (clusterize (diff_obj Stdpp.dummy_loc obj)) l)) + | _ -> assert false ;; let disambiguate_cic_appl_pattern status args = diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli index c9735dbf9..5a9b314c6 100644 --- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli +++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli @@ -43,7 +43,19 @@ class virtual status : method set_disambiguate_status: #g_status -> 'self end -(* val eval_with_new_aliases: +(* reports disambiguation errors *) +exception Error of + (* location of a choice point *) + (Stdpp.location * + (* one possible choice (or no valid choice) *) + (GrafiteAst.alias_spec option * + (* list of asts together with the failing location and error msg *) + ((Stdpp.location * GrafiteAst.alias_spec) list * + Stdpp.location * string) list) + list) + list + + (* val eval_with_new_aliases: #status as 'status -> ('status -> 'a) -> ((Stdpp.location * DisambiguateTypes.domain_item) * GrafiteAst.alias_spec) list * 'a *) diff --git a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml index 1d3242804..ff6f70e94 100644 --- a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml +++ b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml @@ -807,50 +807,42 @@ let disambiguate_term (status: #NCicCoercion.status) ~context ~metasenv ~subst let _ = (aliases : GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t) in let local_names = List.map (fun (n,_) -> n) context in let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in - let res,b = - MultiPassDisambiguator.disambiguate_thing - ~freshen_thing:NotationUtil.freshen_term - ~context ~metasenv ~initial_ugraph:() ~aliases - ~mk_implicit ~description_of_alias ~fix_instance + Disambiguate.disambiguate_thing + ~context ~metasenv ~subst ~use_coercions:true ~string_context_of_context:(List.map (fun (x,_) -> Some x)) - ~universe ~uri:None ~pp_thing:(NotationPp.pp_term status) ~pp_term:(NotationPp.pp_term status) - ~passes:(MultiPassDisambiguator.passes ()) - ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term + ~initial_ugraph:() ~expty + ~mk_implicit ~description_of_alias ~fix_instance ~aliases + ~universe ~lookup_in_library + ~uri:None ~pp_thing:(NotationPp.pp_term status) ~pp_term:(NotationPp.pp_term status) + ~domain_of_thing:Disambiguate.domain_of_term ~interpretate_thing:(interpretate_term status ~obj_context:[] ~mk_choice (?create_dummy_ids:None)) ~refine_thing:(refine_term status) (text,prefix_len, (initialize_ast ~universe ~lookup_in_library ~local_names term)) ~visit:Disambiguate.bfvisit - ~mk_localization_tbl ~expty ~subst - in - List.map (function (t,a,b,c,_) -> t,a,b,c) res, b + ~mk_localization_tbl ;; - let disambiguate_obj (status: #NCicCoercion.status) ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj) = let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in - let res,b = - let obj' = initialize_obj ~universe ~lookup_in_library obj in - MultiPassDisambiguator.disambiguate_thing - ~freshen_thing:NotationUtil.freshen_obj - ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases - ~mk_implicit ~description_of_alias ~fix_instance + let obj' = initialize_obj ~universe ~lookup_in_library obj in + Disambiguate.disambiguate_thing + ~context:[] ~metasenv:[] ~subst:[] ~use_coercions:true ~string_context_of_context:(List.map (fun (x,_) -> Some x)) - ~universe - ~uri:(Some uri) - ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status)) ~pp_term:(NotationPp.pp_term status) - ~passes:(MultiPassDisambiguator.passes ()) - ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj + ~initial_ugraph:() ~expty:None + ~mk_implicit ~description_of_alias ~fix_instance ~aliases + ~universe ~lookup_in_library + ~uri:(Some uri) ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status)) + ~pp_term:(NotationPp.pp_term status) + ~domain_of_thing:Disambiguate.domain_of_obj ~interpretate_thing:(interpretate_obj status ~mk_choice) ~refine_thing:(refine_obj status) (text,prefix_len,obj') ~visit:Disambiguate.bfvisit_obj - ~mk_localization_tbl ~expty:None - in - List.map (function (o,a,b,c,_) -> o,a,b,c) res, b + ~mk_localization_tbl ;; (* let _ = diff --git a/matitaB/components/ng_disambiguation/nCicDisambiguate.mli b/matitaB/components/ng_disambiguation/nCicDisambiguate.mli index b63f8afaa..3423d7921 100644 --- a/matitaB/components/ng_disambiguation/nCicDisambiguate.mli +++ b/matitaB/components/ng_disambiguation/nCicDisambiguate.mli @@ -29,11 +29,7 @@ val disambiguate_term : DisambiguateTypes.Environment.key -> GrafiteAst.alias_spec list) -> NotationPt.term Disambiguate.disambiguator_input -> - (NotationPt.term * - NCic.metasenv * - NCic.substitution * - NCic.term) list * - bool + (GrafiteAst.alias_spec,NotationPt.term,NCic.metasenv,NCic.substitution,NCic.term,unit) Disambiguate.disamb_result val disambiguate_obj : #NCicCoercion.status -> @@ -50,9 +46,6 @@ val disambiguate_obj : GrafiteAst.alias_spec list) -> uri:NUri.uri -> string * int * NotationPt.term NotationPt.obj -> - (NotationPt.term NotationPt.obj * - NCic.metasenv * - NCic.substitution * NCic.obj) - list * bool + (GrafiteAst.alias_spec,NotationPt.term NotationPt.obj,NCic.metasenv,NCic.substitution,NCic.obj,unit) Disambiguate.disamb_result val disambiguate_path: #NCicEnvironment.status -> NotationPt.term -> NCic.term diff --git a/matitaB/components/ng_tactics/nTacStatus.ml b/matitaB/components/ng_tactics/nTacStatus.ml index 3a07acc05..26e4ade40 100644 --- a/matitaB/components/ng_tactics/nTacStatus.ml +++ b/matitaB/components/ng_tactics/nTacStatus.ml @@ -27,7 +27,7 @@ module NRef = NReference let wrap fname f x = try f x with - | MultiPassDisambiguator.DisambiguationError _ + | GrafiteDisambiguate.Error _ | NCicRefiner.RefineFailure _ | NCicUnification.UnificationFailure _ | NCicTypeChecker.TypeCheckerFailure _ diff --git a/matitaB/matita/Makefile b/matitaB/matita/Makefile index ba9baef61..7339eaf41 100644 --- a/matitaB/matita/Makefile +++ b/matitaB/matita/Makefile @@ -52,7 +52,6 @@ MLI = \ predefined_virtuals.mli \ matitaMathView.mli \ matitaScript.mli \ - matitaGui.mli \ $(NULL) CMLI = \ matitaTypes.mli \ @@ -96,7 +95,6 @@ ALL_NORMAL_ML = \ cicMathView.ml \ matitadaemon.ml \ matitaGtkMisc.ml \ - matita.ml \ virtuals.ml \ lablGraphviz.ml \ matitaEngine.ml \ @@ -131,7 +129,7 @@ ALL_SYNTAX_ML = matitaScriptLexer.ml ALL_SYNTAX_MLI = matitaScriptLexer.mli PROGRAMS_BYTE = \ - matita matitac matitadaemon matitaclean + matitac matitadaemon matitaclean PROGRAMS = $(PROGRAMS_BYTE) PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE)) NOINST_PROGRAMS = @@ -200,8 +198,6 @@ links: $(H)ln -sf matitac.opt matitac linkonly: - $(H)echo " OCAMLC matita.ml" - $(H)$(OCAMLC) $(PKGS) -linkpkg -o matita $(CMOS) $(OCAML_DEBUG_FLAGS) matita.ml $(H)echo " OCAMLC matitac.ml" $(H)$(OCAMLC) $(CPKGS) -linkpkg -o matitac $(CCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitac.ml $(H)echo " OCAMLC matitadaemon.ml" diff --git a/matitaB/matita/matitaExcPp.ml b/matitaB/matita/matitaExcPp.ml index e3e18a415..89c04c278 100644 --- a/matitaB/matita/matitaExcPp.ml +++ b/matitaB/matita/matitaExcPp.ml @@ -175,7 +175,7 @@ let rec to_string = None, "NTactic error: " ^ Lazy.force msg | NTacStatus.Error (msg,Some exn) -> None, "NTactic error: " ^ Lazy.force msg ^ "\n" ^ snd(to_string exn) - | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> +(* | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> let loc = match errorll with | ((_,_,loc_msg,_)::_)::_ -> @@ -233,6 +233,6 @@ let rec to_string = in loc, "********** DISAMBIGUATION ERRORS: **********\n" ^ - explain (aux errorll) + explain (aux errorll) *) | exn -> None, "Uncaught exception: " ^ Printexc.to_string exn diff --git a/matitaB/matita/matitaInit.ml b/matitaB/matita/matitaInit.ml index d4a47267f..6307c5f69 100644 --- a/matitaB/matita/matitaInit.ml +++ b/matitaB/matita/matitaInit.ml @@ -229,7 +229,7 @@ let parse_cmdline init_status = ("Do not catch top-level exception " ^ "(useful for backtrace inspection)"); "-onepass", - Arg.Unit (fun () -> MultiPassDisambiguator.only_one_pass := true), + Arg.Unit (fun () -> () (* MultiPassDisambiguator.only_one_pass := true *)), "Enable only one disambiguation pass"; ] else [] diff --git a/matitaB/matita/matitaScript.ml b/matitaB/matita/matitaScript.ml index aa51b36a0..6d703b556 100644 --- a/matitaB/matita/matitaScript.ml +++ b/matitaB/matita/matitaScript.ml @@ -209,10 +209,10 @@ and eval_statement include_paths (buffer : GText.buffer) status script HExtlib.Localized (floc, exn) -> HExtlib.raise_localized_exception ~offset:(MatitaGtkMisc.utf8_string_length parsed_text) floc exn - | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> + (* | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> raise (MultiPassDisambiguator.DisambiguationError - (offset+parsed_text_length, errorll)) + (offset+parsed_text_length, errorll)) *) in assert (text=""); (* no macros inside comments, please! *) let st,text = s in diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 14bcf1db6..6d71ec6bc 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -2,7 +2,7 @@ open Printf;; open Http_types;; exception Emphasized_error of string -exception Ambiguous of string +exception Disamb_error of string module Stack = Continuationals.Stack @@ -401,6 +401,45 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = cgi#out_channel#commit_work() ;; +let xml_of_disamb_error l = + let mk_alias = function + | GrafiteAst.Ident_alias (_,uri) -> "href=\"" ^ uri ^ "\"" + | GrafiteAst.Symbol_alias (_,uri,desc) + | GrafiteAst.Number_alias (uri,desc) -> + let uri = try HExtlib.unopt uri with _ -> "cic:/fakeuri.def(1)" in + "href=\"" ^ uri ^ "\" title=\"" ^ + (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () desc) + ^ "\"" + in + + let mk_interpr (loc,a) = + let x,y = HExtlib.loc_of_floc loc in + Printf.sprintf "" + x y (mk_alias a) + in + + let mk_failure (il,loc,msg) = + let x,y = HExtlib.loc_of_floc loc in + Printf.sprintf "%s" + x y (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () msg) + (String.concat "" (List.map mk_interpr il)) + in + + let mk_choice (a,fl) = + let fl' = String.concat "" (List.map mk_failure fl) in + match a with + | None -> "" ^ fl' ^ "" + | Some a -> Printf.sprintf "%s" (mk_alias a) fl' + in + + let mk_located (loc,cl) = + let x,y = HExtlib.loc_of_floc loc in + Printf.sprintf "%s" + x y (String.concat "" (List.map mk_choice cl)) + in + "" ^ (String.concat "" (List.map mk_located l)) ^ "" +;; + let advance0 sid text = let status = MatitaAuthentication.get_status sid in let history = MatitaAuthentication.get_history sid in @@ -473,7 +512,8 @@ let advance0 sid text = *) let strchoices = Printf.sprintf "%s" x y strchoices - in raise (Ambiguous strchoices) + in raise (Disamb_error strchoices) + | GrafiteDisambiguate.Error l -> raise (Disamb_error (xml_of_disamb_error l)) (* | End_of_file -> ... *) in MatitaAuthentication.set_status sid st; @@ -746,7 +786,7 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string body - | Ambiguous text -> + | Disamb_error text -> let body = "" ^ text ^ "" in cgi # set_header ~cache:`No_cache @@ -773,7 +813,7 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let error_msg = function | Emphasized_error text -> "" ^ text ^ "" - | Ambiguous text -> (* *) text + | Disamb_error text -> text | End_of_file _ -> (* not an error *) "" | e -> (* unmanaged error *) "" ^ diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index d1480e72d..343d539e6 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -586,6 +586,7 @@ function advanceForm1() if (is_defined(xml)) { var parsed = xml.getElementsByTagName("parsed")[0]; var ambiguity = xml.getElementsByTagName("ambiguity")[0]; + var disamberr = xml.getElementsByTagName("disamberror")[0]; if (is_defined(parsed)) { // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND"); var len = parseInt(parsed.getAttribute("length")); @@ -666,6 +667,13 @@ function advanceForm1() matita.disambMode = true; updateSide(); } + else if (is_defined(disamberr)) { + set_cps(disamberr.childNodes); + matita.unlockedbackup = unlocked.innerHTML.html_to_matita(); + matita.disambMode = true; + disable_toparea(); + next_cp(0); + } else { var error = xml.getElementsByTagName("error")[0]; unlocked.innerHTML = error.childNodes[0].wholeText; @@ -681,6 +689,180 @@ function advanceForm1() } +// get or set 's (in case of disamb error) +function get_cps() { + return matita.choicepoints +} + +function set_cps(cps) { + matita.choicepoints = cps; +} + +// get radio buttons for 's in a given cp +function get_choice_opts(i) { + var res = []; + var choices = get_cps()[i].childNodes; + for (var j = 0;j < choices.length;j++) { + var href = choices[j].getAttribute("href"); + var title = choices[j].getAttribute("title"); + var desc; + if (is_defined(title)) { + desc = title; + } else { + desc = href; + } + + res[j] = document.createElement("input"); + res[j].setAttribute("type","radio"); + res[j].setAttribute("name","choice"); + res[j].setAttribute("choicepointno",i); + res[j].setAttribute("choiceno",j); + res[j].setAttribute("href",href); + res[j].setAttribute("title",title); + res[j].setAttribute("desc",desc); + + if (j == 0) res[j].setAttribute("checked",""); + } + return res; +} + +// get radio buttons for 's in a given choice +function get_failure_opts(i,j) { + var res = []; + var failures = get_cps()[i].childNodes[j].childNodes; + for (var k = 0;k < failures.length;k++) { + var start = failures[k].getAttribute("start"); + var stop = failures[k].getAttribute("stop"); + var title = failures[k].getAttribute("title"); + + res[k] = document.createElement("input"); + res[k].setAttribute("type","radio"); + res[k].setAttribute("name","failure"); + res[k].setAttribute("choicepointno",i); + res[k].setAttribute("choiceno",j); + res[k].setAttribute("failureno",k); + res[k].setAttribute("start",start); + res[k].setAttribute("stop",stop); + res[k].setAttribute("title",title); + + if (k == 0) res[k].setAttribute("checked",""); + } + return res; +} + +function next_cp(curcp) { + var cp = get_cps()[curcp]; + var start = parseInt(cp.getAttribute("start")); + var stop = parseInt(cp.getAttribute("stop")); + + matita.errorStart = start; + matita.errorStop = stop; + // matita.unlockedbackup = unlocked.innerHTML.html_to_matita(); + + var unlockedtxt = matita.unlockedbackup; + var pre = unlockedtxt.substring(0,start).matita_to_html(); + var mid = unlockedtxt.substring(start,stop).matita_to_html(); + var post = unlockedtxt.substring(stop).matita_to_html(); + unlocked.innerHTML = pre + + "" + + mid + "" + post; + + var title = "

Disambiguation failed

"; + disambcell.innerHTML = title; + var choices = get_choice_opts(curcp); + for (var i = 0;i < choices.length;i++) { + disambcell.appendChild(choices[i]); + disambcell.appendChild(document.createTextNode(choices[i].getAttribute("desc"))); + disambcell.appendChild(document.createElement("br")); + } + + // update index of the next choicepoint + new_curcp = (curcp + 1) % get_cps().length; + + var okbutton = document.createElement("input"); + okbutton.setAttribute("type","button"); + okbutton.setAttribute("value","OK"); + okbutton.setAttribute("onclick","show_failures()"); + var cancelbutton = document.createElement("input"); + cancelbutton.setAttribute("type","button"); + cancelbutton.setAttribute("value","Close"); + cancelbutton.setAttribute("onclick","cancel_disambiguate()"); + var tryagainbutton = document.createElement("input"); + tryagainbutton.setAttribute("type","button"); + if (new_curcp > 0) { + tryagainbutton.setAttribute("value","Try something else"); + } else { + tryagainbutton.setAttribute("value","Restart"); + } + tryagainbutton.setAttribute("onclick","next_cp(" + new_curcp + ")"); + + disambcell.appendChild(okbutton); + disambcell.appendChild(tryagainbutton); + disambcell.appendChild(cancelbutton); + + //disable_toparea(); + + //matita.disambMode = true; + updateSide(); + +} + +function show_failures() { + + var choice = document.getElementsByName("choice")[get_checked_index("choice")]; + var cpno = parseInt(choice.getAttribute("choicepointno")); + var choiceno = parseInt(choice.getAttribute("choiceno")); + var choicedesc = choice.getAttribute("desc"); + + var title = "

Disambiguation failed

"; + var subtitle = "

Errors at node " + choiceno + " = " + choicedesc + "

"; + + disambcell.innerHTML = title + subtitle; + var failures = get_failure_opts(cpno,choiceno); + for (var i = 0;i < failures.length;i++) { + disambcell.appendChild(failures[i]); + disambcell.appendChild(document.createTextNode(failures[i].getAttribute("title"))); + disambcell.appendChild(document.createElement("br")); + } + + var okbutton = document.createElement("input"); + okbutton.setAttribute("type","button"); + okbutton.setAttribute("value","Show error loc"); + okbutton.setAttribute("onclick","show_err()"); + var cancelbutton = document.createElement("input"); + cancelbutton.setAttribute("type","button"); + cancelbutton.setAttribute("value","Close"); + cancelbutton.setAttribute("onclick","cancel_disambiguate()"); + var backbutton = document.createElement("input"); + backbutton.setAttribute("type","button"); + backbutton.setAttribute("value","<< Back"); + backbutton.setAttribute("onclick","next_cp(" + cpno + ")"); + + disambcell.appendChild(backbutton); + disambcell.appendChild(okbutton); + disambcell.appendChild(cancelbutton); + +} + +function show_err() { + var radios = document.getElementsByName("failure"); + for (i = 0; i < radios.length; i++) { + if (radios[i].checked) { + var start = radios[i].getAttribute("start"); + var stop = radios[i].getAttribute("stop"); + var title = radios[i].getAttribute("title"); + var unlockedtxt = matita.unlockedbackup; + var pre = unlockedtxt.substring(0,start).matita_to_html(); + var mid = unlockedtxt.substring(start,stop).matita_to_html(); + var post = unlockedtxt.substring(stop).matita_to_html(); + unlocked.innerHTML = pre + + "" + + mid + "" + post; + break; + } + } +} + function gotoBottom() { processor = function(xml) { @@ -1272,6 +1454,31 @@ function do_disambiguate() { } } +function do_showerror() { + var i = get_checked_index("choice"); + if (i != null) { + var pre = matita.unlockedbackup + .substring(0,matita.ambiguityStart).matita_to_html(); + var mid = matita.unlockedbackup + .substring(matita.ambiguityStart,matita.ambiguityStop) + .matita_to_html(); + var post = matita.unlockedbackup + .substring(matita.ambiguityStop).matita_to_html(); + + var href = matita.interpretations[i].href; + var title = matita.interpretations[i].title; + + if (is_defined(title)) { + mid = "" + mid + ""; + } else { + mid = "" + mid + ""; + } + + unlocked.innerHTML = pre + mid + post; + + } +} + function readCookie(name) { var nameEQ = name + "="; var ca = document.cookie.split(';'); -- 2.39.2