From 0e3d8e00433a9a4dd72310c1e889814848a96c10 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Mon, 24 Oct 2011 16:40:58 +0000 Subject: [PATCH] Matitaweb: first attempt at web UI for disambiguation. Also includes a rather radical change in the way the graphical layout is handled. --- .../components/disambiguation/disambiguate.ml | 17 +- .../disambiguation/disambiguate.mli | 6 +- .../ng_disambiguation/grafiteDisambiguate.ml | 78 ++++++---- .../ng_disambiguation/grafiteDisambiguate.mli | 3 + matitaB/matita/index.html | 24 +-- matitaB/matita/matitadaemon.ml | 49 ++++-- matitaB/matita/matitaweb.css | 55 +++++-- matitaB/matita/matitaweb.js | 147 +++++++++++++++--- 8 files changed, 285 insertions(+), 94 deletions(-) diff --git a/matitaB/components/disambiguation/disambiguate.ml b/matitaB/components/disambiguation/disambiguate.ml index 5ce1386ae..a65dd3e5f 100644 --- a/matitaB/components/disambiguation/disambiguate.ml +++ b/matitaB/components/disambiguation/disambiguate.ml @@ -31,9 +31,6 @@ open DisambiguateTypes module Ast = NotationPt -(* the integer is an offset to be added to each location *) -exception Ambiguous_input -(* the integer is an offset to be added to each location *) exception NoWellTypedInterpretation of int * ((Stdpp.location list * string * string) list * @@ -51,6 +48,7 @@ type 'a disambiguator_input = string * int * 'a type domain = domain_tree list and domain_tree = Node of Stdpp.location list * domain_item * domain +(* let mono_uris_callback ~selection_mode ?ok ?(enable_button_for_non_vars = true) ~title ~msg ~id = if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true @@ -60,8 +58,8 @@ let mono_uris_callback ~selection_mode ?ok else raise Ambiguous_input -let mono_interp_callback _ _ _ = raise Ambiguous_input -let mono_disamb_callback _ = raise Ambiguous_input +let mono_interp_callback _ _ _ = assert false +let mono_disamb_callback _ = assert false let _choose_uris_callback = ref mono_uris_callback let _choose_interp_callback = ref mono_interp_callback @@ -73,6 +71,8 @@ let set_choose_disamb_callback f = _choose_disamb_callback := f let interactive_user_uri_choice = !_choose_uris_callback let interactive_interpretation_choice interp = !_choose_interp_callback interp let interactive_ast_choice interp = !_choose_disamb_callback interp +*) + let input_or_locate_uri ~(title:string) ?id () = None (* Zack: I try to avoid using this callback. I therefore assume that * the presence of an identifier that can't be resolved via "locate" @@ -730,12 +730,13 @@ let disambiguate_thing in match res with | [] -> raise (NoWellTypedInterpretation (0,[])) + (* XXX : the boolean seems not to play a role any longer *) | [t] -> res,false - | _ -> - let choices = List.map (fun (t,_,_,_,_) -> pp_thing t) res in + | _ -> 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 *) + List.iter pp_thing res; res,true *) *) ;; diff --git a/matitaB/components/disambiguation/disambiguate.mli b/matitaB/components/disambiguation/disambiguate.mli index bb20ff866..2e6677d72 100644 --- a/matitaB/components/disambiguation/disambiguate.mli +++ b/matitaB/components/disambiguation/disambiguate.mli @@ -25,10 +25,6 @@ (** {2 Disambiguation interface} *) -(** raised when ambiguous input is found but not expected (e.g. in the batch - * compiler) *) -exception Ambiguous_input - (* 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 @@ -58,6 +54,7 @@ type ('term,'metasenv,'subst,'graph) test_result = exception Try_again of string Lazy.t +(* val set_choose_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type -> unit @@ -76,6 +73,7 @@ val mono_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type * choose_interp_callback if not set otherwise with set_choose_interp_callback * above *) val mono_interp_callback: DisambiguateTypes.interactive_interpretation_choice_type +*) val resolve : env:'alias1 DisambiguateTypes.InterprEnv.t -> diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml index 9c7ea4768..b1dc98a1e 100644 --- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml +++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml @@ -76,6 +76,9 @@ class virtual status uid = new_aliases,res ;;*) +(* reports the first source of ambiguity and its possible interpretations *) +exception Ambiguous_input of (Stdpp.location * GrafiteAst.alias_spec 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)) @@ -107,15 +110,6 @@ let add_to_disambiguation_univ status new_aliases = exception BaseUriNotSetYet -let singleton msg = function - | [x], _ -> x - | l, _ -> - let debug = - Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations" - msg (List.length l) - in - prerr_endline debug; assert false - let __Implicit = "__Implicit__" let __Closed_Implicit = "__Closed_Implicit__" @@ -297,11 +291,24 @@ let diff_obj loc o1 o2 = match o1,o2 with | _ -> assert false ;; +(* this function, called on a list of choices that must + * be different, never fails and returns the location of + * the first ambiguity (and its possible interpretations) *) +let rec find_diffs l = + let loc,_ = List.hd (List.hd l) in + let hds = List.map (fun x -> snd (List.hd x)) l in + let uniq_hds = HExtlib.list_uniq hds in + + if List.length uniq_hds > 1 + then loc, uniq_hds + else + let tls = List.map List.tl l in + find_diffs tls +;; + let disambiguate_nterm status expty context metasenv subst thing -= - let newast, metasenv, subst, cic = - singleton "first" - (NCicDisambiguate.disambiguate_term += + let choices, _ = NCicDisambiguate.disambiguate_term status ~aliases:status#disambiguate_db.interpr ~expty @@ -310,16 +317,24 @@ let disambiguate_nterm status expty context metasenv subst thing ~mk_choice:(ncic_mk_choice status) ~mk_implicit ~fix_instance ~description_of_alias:GrafiteAst.description_of_alias - ~context ~metasenv ~subst thing) + ~context ~metasenv ~subst thing in let _,_,thing' = thing in - let diff = diff_term Stdpp.dummy_loc thing' newast in - let status = add_to_interpr status diff - in - metasenv, subst, status, cic + match choices with + | [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 + | _ -> + let diffs = + List.map (fun (ast,_,_,_) -> + diff_term Stdpp.dummy_loc thing' ast) choices + in + raise (Ambiguous_input (find_diffs diffs)) ;; - type pattern = NotationPt.term Disambiguate.disambiguator_input option * (string * NCic.term) list * NCic.term option @@ -367,7 +382,7 @@ let disambiguate_just disambiguate_term context metasenv = metasenv, `Auto params ;; -let disambiguate_nobj status ?baseuri (text,prefix_len,obj) = +let disambiguate_nobj status ?baseuri (text,prefix_len,obj as obj') = let uri = let baseuri = match baseuri with Some x -> x | None -> raise BaseUriNotSetYet @@ -381,9 +396,8 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) = in NUri.uri_of_string (baseuri ^ "/" ^ name) in - let ast, _, _, cic = - singleton "third" - (NCicDisambiguate.disambiguate_obj + + let choices, _ = NCicDisambiguate.disambiguate_obj status ~lookup_in_library:(nlookup_in_library status) ~description_of_alias:GrafiteAst.description_of_alias @@ -391,11 +405,21 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) = ~mk_implicit ~fix_instance ~uri ~aliases:status#disambiguate_db.interpr ~universe:(status#disambiguate_db.multi_aliases) - (text,prefix_len,obj)) in - let diff = diff_obj Stdpp.dummy_loc obj ast in - let status = add_to_interpr status diff + obj' in - status, cic + 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 + | _ -> + let diffs = + List.map (fun (ast,_,_,_) -> + diff_obj Stdpp.dummy_loc obj ast) choices + in + raise (Ambiguous_input (find_diffs diffs)) ;; let disambiguate_cic_appl_pattern status args = diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli index e71c25b82..c9735dbf9 100644 --- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli +++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli @@ -65,6 +65,9 @@ val aliases_for_objs: (* args: print function, message (may be empty), status *) val dump_aliases: (string -> unit) -> string -> #status -> unit +(* reports the first source of ambiguity and its possible interpretations *) +exception Ambiguous_input of (Stdpp.location * GrafiteAst.alias_spec list) + exception BaseUriNotSetYet val disambiguate_nterm : diff --git a/matitaB/matita/index.html b/matitaB/matita/index.html index d3fe3491f..80f49ece4 100644 --- a/matitaB/matita/index.html +++ b/matitaB/matita/index.html @@ -3,6 +3,7 @@ + @@ -10,19 +11,19 @@ - + - + -
+
-
+

Matita - <<Filename>>

-
+ -
+
+
+
-
+ 

   

+ 

 

 

 
@@ -92,7 +96,7 @@