From: Wilmer Ricciotti Date: Tue, 27 Mar 2012 12:23:00 +0000 (+0000) Subject: Matitaweb: X-Git-Tag: make_still_working~1833 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c81b0e8dbfe80e2350e9322afa8316f39f98c3b3;p=helm.git Matitaweb: Improved support for notations enriched with hyperlinks. This revision introduces a "ref" keyword which can be used in the lefthand side of notation statements. "ref" can only be used to decorate literals (i.e. symbols, numbers, or keywords). The syntax is as follows: LITERAL ::= SIMPLE_LITERAL | ref CSYMBOL SIMPLE_LITERAL For example, the notation ref 'cons [ list0 x sep ; ref 'nil ] used as the compact notation for lists specifies that the `[' symbol will be enriched with the interpretation of 'cons nodes of the AST, and the `]' symbol with the interpretation of 'nil nodes of the AST. --- diff --git a/matitaB/components/content/notationEnv.ml b/matitaB/components/content/notationEnv.ml index eb85ec038..6951760bf 100644 --- a/matitaB/components/content/notationEnv.ml +++ b/matitaB/components/content/notationEnv.ml @@ -37,7 +37,10 @@ type value = | NumValue of string | OptValue of value option | ListValue of value list - | DisambiguationValue of (Stdpp.location * string option * string option) + (* optional name of Ast.Symbols that we want to contain the interpretation of this literal + * location of the literal we are parsing + * optional uri, optional desc *) + | DisambiguationValue of (string option * Stdpp.location * string option * string option) type value_type = | TermType of int (* the level of the expected term *) diff --git a/matitaB/components/content/notationEnv.mli b/matitaB/components/content/notationEnv.mli index 311889321..69ffceb0c 100644 --- a/matitaB/components/content/notationEnv.mli +++ b/matitaB/components/content/notationEnv.mli @@ -35,7 +35,7 @@ type value = | NumValue of string | OptValue of value option | ListValue of value list - | DisambiguationValue of (Stdpp.location * string option * string option) + | DisambiguationValue of (string option * Stdpp.location * string option * string option) type value_type = | TermType of int (* the level of the expected term *) diff --git a/matitaB/components/content/notationPp.ml b/matitaB/components/content/notationPp.ml index 50ccb16b4..a69ca90ab 100644 --- a/matitaB/components/content/notationPp.ml +++ b/matitaB/components/content/notationPp.ml @@ -42,15 +42,17 @@ let pp_binder = function | `Exists -> "exists" | `Forall -> "forall" -let pp_literal = +(* XXX: ignoring the optional CSYMBOL + * (it's fine if this is only used for pretty printing output notations) *) +let pp_literal (_,t) = if debug_printing then - (function (* debugging version *) - | `Symbol _ as t -> + (match t with (* debugging version *) + | `Symbol _ -> sprintf "symbol(%s)" (NotationUtil.string_of_literal t) - | `Keyword _ as t -> + | `Keyword _ -> sprintf "keyword(%s)" (NotationUtil.string_of_literal t) - | `Number _ as t -> sprintf "number(%s)" (NotationUtil.string_of_literal t)) - else NotationUtil.string_of_literal + | `Number _ -> sprintf "number(%s)" (NotationUtil.string_of_literal t)) + else NotationUtil.string_of_literal t let pp_pos = function @@ -271,7 +273,7 @@ and pp_fold_kind = function and pp_sep_opt = function | None -> "" - | Some sep -> sprintf " sep %s" (pp_literal sep) + | Some sep -> sprintf " sep %s" (pp_literal (None,sep)) and pp_variable = function | Ast.NumVar s -> "number " ^ s diff --git a/matitaB/components/content/notationPt.ml b/matitaB/components/content/notationPt.ml index b624c9a86..4804208f0 100644 --- a/matitaB/components/content/notationPt.ml +++ b/matitaB/components/content/notationPt.ml @@ -62,7 +62,7 @@ type 'term capture_variable = 'term * 'term option (** To be increased each time the term type below changes, used for "safe" * marshalling *) -let magic = 7 +let magic = 8 type term = (* CIC AST *) @@ -101,8 +101,9 @@ type term = | NCic of NCic.term (* Syntax pattern extensions *) - - | Literal of literal + (* string option = optional name of an Ast.Symbol occurring in the level 2 + * term, which is associated to this literal *) + | Literal of (string option * literal) | Layout of layout_pattern | Magic of magic_term diff --git a/matitaB/components/content/notationUtil.ml b/matitaB/components/content/notationUtil.ml index d047eb58e..dc914932a 100644 --- a/matitaB/components/content/notationUtil.ml +++ b/matitaB/components/content/notationUtil.ml @@ -157,7 +157,7 @@ let keywords_of_term t = let rec aux = function | Ast.AttributedTerm (_, t) -> aux t | Ast.Layout l -> Ast.Layout (visit_layout aux l) - | Ast.Literal (`Keyword (k,_)) as t -> + | Ast.Literal (_,`Keyword (k,_)) as t -> add_keyword k; t | Ast.Literal _ as t -> t @@ -179,7 +179,7 @@ let rec strip_attributes t = let rec get_idrefs = function - | Ast.Symbol (_,Some (_,desc)) -> [desc] + | Ast.Symbol (csym,Some (uri,desc)) -> [csym,uri,desc] | _ -> [] let meta_names_of_term term = diff --git a/matitaB/components/content/notationUtil.mli b/matitaB/components/content/notationUtil.mli index 981030d49..6d5919d93 100644 --- a/matitaB/components/content/notationUtil.mli +++ b/matitaB/components/content/notationUtil.mli @@ -62,7 +62,7 @@ val visit_variable: val strip_attributes: NotationPt.term -> NotationPt.term (** @return the list of proper (i.e. non recursive) IdRef of a term *) -val get_idrefs: NotationPt.term -> string list +val get_idrefs: NotationPt.term -> (string * string option * string) list (** generalization of List.combine to n lists *) val ncombine: 'a list list -> 'a list list diff --git a/matitaB/components/content_pres/cicNotationLexer.ml b/matitaB/components/content_pres/cicNotationLexer.ml index 3c84e0bb5..b7451bc78 100644 --- a/matitaB/components/content_pres/cicNotationLexer.ml +++ b/matitaB/components/content_pres/cicNotationLexer.ml @@ -130,11 +130,11 @@ let level1_keywords = "break"; "list0"; "list1"; "sep"; "opt"; - "term"; "ident"; "number"; + "term"; "ident"; "number"; "ref" ] @ level1_layouts let level2_meta_keywords = - [ "if"; "then"; "elCicNotationParser.se"; + [ "if"; "then"; "else"; "fold"; "left"; "right"; "rec"; "fail"; "default"; @@ -463,10 +463,14 @@ let rec level1_pattern_token = lexer | utf8_blank+ -> ligatures_token level1_pattern_token lexbuf | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf) - | hreftag -> return lexbuf ("ATAG", "") +(* | hreftag -> return lexbuf ("ATAG", "") | hrefclose -> return lexbuf ("ATAGEND","") | generictag - | closetag -> ligatures_token level1_pattern_token lexbuf + | closetag -> ligatures_token level1_pattern_token lexbuf *) + | qkeyword -> + return lexbuf ("QKEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf)) + | csymbol -> prerr_endline ("lexing csymbol " ^ (Ulexing.utf8_lexeme lexbuf)); + return lexbuf ("CSYMBOL", remove_left_quote (Ulexing.utf8_lexeme lexbuf)) | ident -> handle_keywords lexbuf (fun x -> List.mem x level1_keywords) "IDENT" | variable_ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf) | pident-> handle_keywords lexbuf (fun x->List.mem x level1_keywords) "PIDENT" @@ -476,8 +480,6 @@ let rec level1_pattern_token = | floatwithunit -> return lexbuf ("FLOATWITHUNIT", Ulexing.utf8_lexeme lexbuf) | tex_token -> return lexbuf (expand_macro lexbuf) - | qkeyword -> - return lexbuf ("QKEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf)) | '(' -> return lexbuf ("LPAREN", "") | ')' -> return lexbuf ("RPAREN", "") | eof -> return_eoi lexbuf diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml index fcd209307..660371552 100644 --- a/matitaB/components/content_pres/cicNotationParser.ml +++ b/matitaB/components/content_pres/cicNotationParser.ml @@ -63,7 +63,7 @@ let refresh_uri_in_checked_l1_pattern ~refresh_uri_in_term ~refresh_uri_in_reference t, n) type binding = - | NoBinding + | NoBinding of string option (* name of Ast.Symbol associated to this literal *) | Binding of string * Env.value_type | Env of (string * Env.value_type) list @@ -189,16 +189,17 @@ let make_action status action bindings = let rec aux (vl : NotationEnv.t) = function [] -> Gramext.action (fun (loc: Ast.location) -> action vl loc) - | NoBinding :: tl -> + | NoBinding csym :: tl -> Gramext.action (fun ((*_,*)(loc: Ast.location)) -> let uri,desc = try + let a,b = HExtlib.loc_of_floc loc in CicNotationLexer.LocalizeEnv.find loc !(status#notation_parser_db.loctable) with Not_found -> None, None in aux (("",(Env.NoType, - Env.DisambiguationValue (loc,uri,desc)))::vl) tl) + Env.DisambiguationValue (csym,loc,uri,desc)))::vl) tl) (* LUCA: DEFCON 3 BEGIN *) | Binding (name, Env.TermType l) :: tl -> Gramext.action @@ -231,7 +232,7 @@ let flatten_opt = let rec aux acc = function [] -> List.rev acc - | NoBinding :: tl -> aux acc tl + | NoBinding _ :: tl -> aux acc tl | Env names :: tl -> aux (List.rev names @ acc) tl | Binding (name, ty) :: tl -> aux ((name, ty) :: acc) tl in @@ -250,12 +251,12 @@ let update_sym_grammar status pattern = assert false and aux_literal status = function - | `Symbol (s,_) -> add_item_to_grammar status (`Sym s) - | `Keyword (s,_) -> + | _,`Symbol (s,_) -> add_item_to_grammar status (`Sym s) + | _,`Keyword (s,_) -> if not (List.mem s CicNotationLexer.initial_keywords) then add_item_to_grammar status (`Kwd s) else status - | `Number _ -> status + | _,`Number _ -> status and aux_layout status = function | Ast.Sub (p1, p2) -> aux (aux status p1) p2 | Ast.Sup (p1, p2) -> aux (aux status p1) p2 @@ -279,7 +280,7 @@ let update_sym_grammar status pattern = | Ast.List0 (p, s) | Ast.List1 (p, s) -> let status = - match s with None -> status | Some s' -> aux_literal status s' + match s with None -> status | Some s' -> aux_literal status (None,s') in aux status p | _ -> assert false @@ -300,24 +301,24 @@ let extract_term_production status pattern = assert false and aux_literal = function - | `Symbol (s,_) -> [NoBinding, gram_symbol status s] - | `Keyword (s,_) -> + | csym,`Symbol (s,_) -> [NoBinding csym, gram_symbol status s] + | csym,`Keyword (s,_) -> (* assumption: s will be registered as a keyword with the lexer *) - [NoBinding, gram_keyword status s] - | `Number (s,_) -> [NoBinding, gram_number s] + [NoBinding csym, gram_keyword status s] + | csym,`Number (s,_) -> [NoBinding csym, gram_number s] and aux_layout = function - | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sub "] @ aux p2 - | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sup "] @ aux p2 - | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\below "] @ aux p2 - | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\above "] @ aux p2 - | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\frac "] @ aux p2 - | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol status "\\infrule "] @ aux p1 @ aux p2 @ aux p3 - | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\atop "] @ aux p2 - | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\over "] @ aux p2 + | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\sub "] @ aux p2 + | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\sup "] @ aux p2 + | Ast.Below (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\below "] @ aux p2 + | Ast.Above (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\above "] @ aux p2 + | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\frac "] @ aux p2 + | Ast.InfRule (p1, p2, p3) -> [NoBinding None, gram_symbol status "\\infrule "] @ aux p1 @ aux p2 @ aux p3 + | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\atop "] @ aux p2 + | Ast.Over (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\over "] @ aux p2 | Ast.Root (p1, p2) -> - [NoBinding, gram_symbol status "\\root "] @ aux p2 - @ [NoBinding, gram_symbol status "\\of "] @ aux p1 - | Ast.Sqrt p -> [NoBinding, gram_symbol status "\\sqrt "] @ aux p + [NoBinding None, gram_symbol status "\\root "] @ aux p2 + @ [NoBinding None, gram_symbol status "\\of "] @ aux p1 + | Ast.Sqrt p -> [NoBinding None, gram_symbol status "\\sqrt "] @ aux p | Ast.Break -> [] | Ast.Box (_, pl) -> List.flatten (List.map aux pl) | Ast.Group pl -> List.flatten (List.map aux pl) @@ -560,6 +561,14 @@ EXTEND | n = NUMBER -> `Number (n,(None,None)) ] ]; + rliteral: [ + [ csymname = OPT [ "ref" ; csymname = CSYMBOL -> + prerr_endline ("parser in rliteral (ref " ^ csymname ^ ")"); + csymname ]; + lit = literal -> + csymname, lit + ] + ]; sep: [ [ "sep"; sep = literal -> sep ] ]; l1_magic_pattern: [ [ "list0"; p = l1_simple_pattern; sep = OPT sep -> @@ -649,7 +658,7 @@ EXTEND return_term_of_level loc (fun l -> Ast.Magic (m l)) | v = l1_pattern_variable -> return_term_of_level loc (fun _ -> Ast.Variable v) - | l = literal -> return_term_of_level loc (fun _ -> Ast.Literal l) + | l = rliteral -> return_term_of_level loc (fun _ -> Ast.Literal l) ] ]; END diff --git a/matitaB/components/content_pres/cicNotationPres.ml b/matitaB/components/content_pres/cicNotationPres.ml index b99851add..553ab1ae1 100644 --- a/matitaB/components/content_pres/cicNotationPres.ml +++ b/matitaB/components/content_pres/cicNotationPres.ml @@ -130,9 +130,9 @@ let render status ?(prec=(-1)) = Box.H ([], (Box.Text ([], "?"^string_of_int n):: (if (l <> []) then [Box.H ([],local_context)] else []))) - | A.Literal (`Symbol (s,x)) - | A.Literal (`Keyword (s,x)) - | A.Literal (`Number (s,x)) -> + | A.Literal (_,`Symbol (s,x)) + | A.Literal (_,`Keyword (s,x)) + | A.Literal (_,`Number (s,x)) -> let attr = match x with | None, None -> [] diff --git a/matitaB/components/content_pres/content2presMatcher.ml b/matitaB/components/content_pres/content2presMatcher.ml index 5eeed2667..0020f8170 100644 --- a/matitaB/components/content_pres/content2presMatcher.ml +++ b/matitaB/components/content_pres/content2presMatcher.ml @@ -183,19 +183,19 @@ struct let env'' = Env.remove_name env' acc_name in match aux acc with | None -> aux_base term - | Some (base_env, ctors', rec_envl) -> - let ctors'' = ctors' @ ctors in + | Some (base_env, ctors_acc, rec_envl) -> + let ctors'' = ctors' @ ctors_acc (* @ ctors *)in Some (base_env, ctors'',env'' :: rec_envl) end in match aux term with | None -> None - | Some (base_env, ctors, rec_envl) -> + | Some (base_env, ctors_term, rec_envl) -> let env' = base_env @ Env.coalesce_env p_rec_decls rec_envl @ env (* @ env LUCA!!! *) in - Some (env', ctors)) + Some (env', ctors_term @ ctors)) | Ast.Default (p_some, p_none) -> (* p_none can't bound names *) let p_some_decls = Env.declarations_of_term p_some in diff --git a/matitaB/components/content_pres/termContentPres.ml b/matitaB/components/content_pres/termContentPres.ml index 13c70be47..212c2cdc0 100644 --- a/matitaB/components/content_pres/termContentPres.ml +++ b/matitaB/components/content_pres/termContentPres.ml @@ -66,13 +66,13 @@ let vbox = box Ast.V let hvbox = box Ast.HV let hovbox = box Ast.HOV let break = Ast.Layout Ast.Break -let space = Ast.Literal (`Symbol (" ", (None,None))) -let builtin_symbol s = Ast.Literal (`Symbol (s,(None,None))) -let keyword k = add_keyword_attrs (Ast.Literal (`Keyword (k,(None,None)))) +let space = Ast.Literal (None,`Symbol (" ", (None,None))) +let builtin_symbol s = Ast.Literal (None,`Symbol (s,(None,None))) +let keyword k = add_keyword_attrs (Ast.Literal (None,`Keyword (k,(None,None)))) let number s = add_xml_attrs (* (RenderingAttrs.number_attributes `MathML) *) () - (Ast.Literal (`Number (s,(None,None)))) + (Ast.Literal (None,`Number (s,(None,None)))) let ident i = add_xml_attrs (* (RenderingAttrs.ident_attributes `MathML) *) () @@ -375,15 +375,27 @@ let instantiate21 idrefs env l1 = in [ value ] | Ast.Magic m -> subst_magic pos env m - | Ast.Literal l as t -> - (match idrefs with - | [] -> [t] - | desc::_ -> + | Ast.Literal (csym,l) as t -> + let enrich_literal l (_,uri,desc) = let desc = Some desc in - (match l with - | `Keyword (k,_) -> [ Ast.Literal (`Keyword (k,(None,desc))) ] - | `Symbol (s,_) -> [ Ast.Literal (`Symbol (s,(None,desc))) ] - | `Number (n,_) -> [ Ast.Literal (`Number (n,(None,desc))) ])) + match l with + | `Keyword (k,_) -> [ Ast.Literal (csym,`Keyword (k,(uri,desc))) ] + | `Symbol (s,_) -> [ Ast.Literal (csym,`Symbol (s,(uri,desc))) ] + | `Number (n,_) -> [ Ast.Literal (csym,`Number (n,(uri,desc))) ] + in + (match csym,idrefs with + | None, [] -> [t] + | None,disamb::_ -> enrich_literal l disamb + | Some cs,_ -> + (try + let disamb = List.find (fun (cs',_,_) -> cs = cs') idrefs in + enrich_literal l disamb + with Not_found -> + (* prerr_endline ("can't find idref for " ^ cs ^ ". Will now print idrefs"); + List.iter + (fun (cs'',_,_) -> prerr_endline ("idref " ^ cs'')) + idrefs;*) + [t])) | Ast.Layout l -> [ Ast.Layout (subst_layout pos env l) ] | t -> [ NotationUtil.visit_ast (subst_singleton pos env) t ] and subst_magic pos env = function @@ -397,7 +409,7 @@ let instantiate21 idrefs env l1 = let sep = match sep_opt with | None -> [] - | Some l -> [ Ast.Literal l; break; space ] + | Some l -> [ Ast.Literal (None,l); break; space ] in let rec instantiate_list acc = function | [] -> List.rev acc @@ -560,15 +572,17 @@ let unopt_names names env = let head_names names env = let rec aux acc = function - | (name, (ty, v)) :: tl when List.mem name names -> + | (name, (ty, v)) as x :: tl when List.mem name names -> (match ty, v with | Env.ListType ty, Env.ListValue (v :: _) -> - aux ((name, (ty, v)) :: acc) tl + aux ((name, (ty,v)):: acc) tl | Env.TermType _, Env.TermValue _ -> - aux ((name, (ty, v)) :: acc) tl + aux (x :: acc) tl | Env.OptType _, Env.OptValue _ -> - aux ((name, (ty, v)) :: acc) tl + aux (x :: acc) tl | _ -> assert false) + | (_,(_,Env.DisambiguationValue _)) as x :: tl -> + aux (x::acc) tl | _ :: tl -> aux acc tl (* base pattern may contain only meta names, thus we trash all others *) | [] -> acc @@ -591,7 +605,7 @@ let tail_names names env = in aux [] env -let instantiate_level2 status env (loc,uri,desc) term = +let instantiate_level2 status env (* (loc,uri,desc) *) term = (* prerr_endline ("istanzio: " ^ NotationPp.pp_term term); *) let fresh_env = ref [] in let lookup_fresh_name n = @@ -623,7 +637,7 @@ let instantiate_level2 status env (loc,uri,desc) term = | Ast.Num _ | Ast.Sort _ | Ast.UserInput -> term - | Ast.Symbol (s,_) -> aux_symbol s loc (uri,desc) + | Ast.Symbol (s,_) -> aux_symbol s (List.map (fun (_,(_,x)) -> x) env) | Ast.Magic magic -> aux_magic env magic | Ast.Variable var -> aux_variable env var @@ -631,10 +645,33 @@ let instantiate_level2 status env (loc,uri,desc) term = | Ast.Cast (t, ty) -> Ast.Cast (aux env t, aux env ty) | _ -> assert false - and aux_symbol s loc = function - | _, None -> Ast.AttributedTerm (`Loc loc, Ast.Symbol (s, None)) - | uri, Some desc -> - Ast.AttributedTerm (`Loc loc, Ast.Symbol (s, Some (uri,desc))) + and aux_symbol s env = + (* XXX: it's totally unclear why the env we receive here is in reverse + * order (a diff with the previous revision shows no obvious reason). + * This one-line patch is needed so that the default symbol chosen for + * storing the interpretation is the leftmost, rather than the rightmost *) + let env = List.rev env in + try + (let dv = + try List.find (function + | Env.DisambiguationValue(Some s',_,_,_) when s = s' -> true + | _ -> false) env + with Not_found -> + List.find (function + | Env.DisambiguationValue(None,_,_,_) -> true + | _ -> false) env + in + match dv with + | Env.DisambiguationValue(_,loc,uri,Some desc) -> + Ast.AttributedTerm (`Loc loc, Ast.Symbol (s, Some (uri,desc))) + | Env.DisambiguationValue(_,loc,_,_) -> + (* The important disambiguation info for symbols is the desc, + * if we don't have it, we won't use the uri either *) + Ast.AttributedTerm (`Loc loc, Ast.Symbol (s, None)) + | _ -> assert false) (* vacuous *) + with Not_found -> + (* Ast.AttributedTerm (`Loc Stdpp.dummy_loc, Ast.Symbol (s, None))*) + Ast.Symbol (s, None) and aux_opt env = function | Some term -> Some (aux env term) | None -> None diff --git a/matitaB/components/content_pres/termContentPres.mli b/matitaB/components/content_pres/termContentPres.mli index 34e63aa64..f64bfcd67 100644 --- a/matitaB/components/content_pres/termContentPres.mli +++ b/matitaB/components/content_pres/termContentPres.mli @@ -56,5 +56,4 @@ val pp_ast: #status -> NotationPt.term -> NotationPt.term (** fills a term pattern instantiating variable magics *) val instantiate_level2: #NCic.status -> NotationEnv.t -> - Stdpp.location * string option * string option -> NotationPt.term -> NotationPt.term diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml index bcbaa93ad..02dfb0012 100644 --- a/matitaB/components/grafite_engine/grafiteEngine.ml +++ b/matitaB/components/grafite_engine/grafiteEngine.ml @@ -34,7 +34,7 @@ type options = { do_heavy_checks: bool ; } -let prerr_endline _ = () +let prerr_endline _ = () let basic_eval_unification_hint (t,n) status = NCicUnifHint.add_user_provided_hint status t n @@ -136,12 +136,13 @@ let eval_alias status data= let basic_eval_input_notation (l1,l2) status = GrafiteParser.extend status l1 (fun env loc -> - let rec get_disamb = function + (* let rec get_disamb = function | [] -> Stdpp.dummy_loc,None,None - | (_,(NotationEnv.NoType,NotationEnv.DisambiguationValue dv))::_ -> dv + | (_,(csym,NotationEnv.NoType,NotationEnv.DisambiguationValue dv))::_ -> dv | _::tl -> get_disamb tl - in - let l2' = TermContentPres.instantiate_level2 status env (get_disamb env) l2 in + in *) + let l2' = + TermContentPres.instantiate_level2 status env (*(get_disamb env)*) l2 in prerr_endline ("new l2 ast : " ^ (NotationPp.pp_term status l2')); NotationPt.AttributedTerm (`Loc loc,l2')) ;; diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml index 162e172a4..d6e4e0c35 100644 --- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml +++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml @@ -106,7 +106,23 @@ let add_to_interpr status new_aliases = {status#disambiguate_db with interpr = interpr } in status#set_disambiguate_db new_status - + +(* +let print_interpr status = + DisambiguateTypes.InterprEnv.iter + (fun loc alias -> + let start,stop = HExtlib.loc_of_floc loc in + let strpos = Printf.sprintf "@(%d,%d):" start stop in + match alias with + | GrafiteAst.Ident_alias (id,uri) -> + Printf.printf "%s [%s;%s]\n" strpos id uri + | GrafiteAst.Symbol_alias (name,_ouri,desc) -> + Printf.printf "%s <%s:%s>\n" strpos name desc + | GrafiteAst.Number_alias (_ouri,desc) -> + Printf.printf "%s \n" strpos desc) + status#disambiguate_db.interpr +*) + let add_to_disambiguation_univ status new_aliases = let multi_aliases = List.fold_left (fun acc (d,c) -> diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli index 5a9b314c6..fd9615cde 100644 --- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli +++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli @@ -66,6 +66,9 @@ val add_to_interpr: #status as 'status -> (Stdpp.location * GrafiteAst.alias_spec) list -> 'status +(* val print_interpr: + #status as 'status -> unit *) + val add_to_disambiguation_univ: #status as 'status -> (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -> 'status diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml index 734140ad3..3757b177f 100644 --- a/matitaB/matita/matitaEngine.ml +++ b/matitaB/matita/matitaEngine.ml @@ -135,7 +135,7 @@ let baseuri_of_script ~include_paths fname = let rec get_ast status ~compiling ~asserted ~include_paths strm = match GrafiteParser.parse_statement status strm with (GrafiteAst.Executable - (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd + (loc,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd -> let already_included = NCicLibrary.get_transitively_included status in let asserted,_ = @@ -156,7 +156,6 @@ and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status match cont with | None -> asserted, true, status, str | Some (asserted,ast) -> - (* pp_ast_statement status ast; *) cb status ast; let status = eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) @@ -172,7 +171,7 @@ and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status in asserted, false, status, str with exn when not matita_debug -> - prerr_endline ("EnrichedWithStatus: " ^ Printexc.to_string exn); + (* prerr_endline ("EnrichedWithStatus: " ^ Printexc.to_string exn); *) raise (EnrichedWithStatus (exn, status)) in if stop then asserted,status else loop asserted status str @@ -251,13 +250,11 @@ and compile ~compiling ~asserted ~include_paths ~outch ?uid fname = HLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); pp_times fname true big_bang big_bang_u big_bang_s; - prerr_endline ("now generating disambiguated script for " ^ fname); let origbuf = Ulexing.from_utf8_channel (open_in fname) in let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in let outstr = ref "" in ignore (SmallLexer.mk_small_printer interpr outstr origbuf); Printf.fprintf outch "%s" !outstr; - prerr_endline ("returning after compilation of " ^ fname); asserted (* MATITA 1.0: debbo fare time_travel sulla ng_library? LexiconSync.time_travel @@ -281,8 +278,8 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid let ngtime_of baseuri = let ngpath = NCicLibrary.ng_path_of_baseuri uid baseuri in let uid = match uid with Some u -> "Some " ^ u | _ -> "None" in - prerr_endline ("uid = " ^ uid); - prerr_endline ("ngpath = " ^ ngpath); + (* prerr_endline ("uid = " ^ uid); + prerr_endline ("ngpath = " ^ ngpath); *) try Some (Unix.stat ngpath).Unix.st_mtime with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in @@ -314,7 +311,7 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid asserted, children_bad || matime > ngtime | None -> asserted,true in - prerr_endline ("asserted = " ^ (String.concat "," asserted)); + (* prerr_endline ("asserted = " ^ (String.concat "," asserted)); *) if not to_be_compiled then fullmapath::asserted,false else if List.mem baseuri already_included then @@ -326,7 +323,7 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid | None -> open_out (fullmapath ^ ".mad"), true | Some c -> c, false in - prerr_endline ("compiling " ^ fullmapath); + (* prerr_endline ("compiling " ^ fullmapath); *) let asserted = compile ~compiling ~asserted ~include_paths ~outch ?uid fullmapath in if is_file_ch then close_out outch; fullmapath::asserted,true diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 0c0f6cefd..1e5a0c700 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -6,6 +6,7 @@ exception Disamb_error of string module Stack = Continuationals.Stack +let debug = prerr_endline (* disable for debug *) let prerr_endline _ = () @@ -348,7 +349,8 @@ let load_doc filename outchan = Http_daemon.respond ~headers:["Content-Type", contenttype] ~code:(`Code 200) ~body:s outchan ;; -let retrieve (cgi : Netcgi.cgi_activation) = +let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in @@ -538,13 +540,20 @@ let advance0 sid text = in raise (Disamb_error strchoices) | GrafiteDisambiguate.Error l -> raise (Disamb_error (xml_of_disamb_error l)) (* | End_of_file -> ... *) - | e -> raise e + | e -> + prerr_endline ("matitadaemon *** Unhandled exception " ^ Printexc.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"; MatitaAuthentication.set_status sid st; MatitaAuthentication.set_history sid (st::history); (* prerr_endline "previous timestamp"; @@ -555,7 +564,8 @@ let advance0 sid text = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (html_of_matita new_statements), new_unparsed, st -let register (cgi : Netcgi.cgi_activation) = +let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let _env = cgi#environment in assert (cgi#arguments <> []); @@ -587,7 +597,8 @@ let register (cgi : Netcgi.cgi_activation) = cgi#out_channel#commit_work() ;; -let login (cgi : Netcgi.cgi_activation) = +let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in assert (cgi#arguments <> []); @@ -617,7 +628,8 @@ let login (cgi : Netcgi.cgi_activation) = cgi#out_channel#commit_work() ;; -let logout (cgi : Netcgi.cgi_activation) = +let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in @@ -641,7 +653,8 @@ let logout (cgi : Netcgi.cgi_activation) = exception File_already_exists;; -let save (cgi : Netcgi.cgi_activation) = +let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in @@ -707,7 +720,8 @@ let save (cgi : Netcgi.cgi_activation) = cgi#out_channel#commit_work() ;; -let initiate_commit (cgi : Netcgi.cgi_activation) = +let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in @@ -732,7 +746,8 @@ let initiate_commit (cgi : Netcgi.cgi_activation) = cgi#out_channel#commit_work() ;; -let svn_update (cgi : Netcgi.cgi_activation) = +let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in @@ -777,8 +792,8 @@ let svn_update (cgi : Netcgi.cgi_activation) = (* returns the length of the executed text and an html representation of the * current metasenv*) (*let advance =*) -let advance (cgi : Netcgi.cgi_activation) = - (* let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in *) +let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in @@ -830,7 +845,8 @@ let advance (cgi : Netcgi.cgi_activation) = cgi#out_channel#commit_work() ;; -let gotoBottom (cgi : Netcgi.cgi_activation) = +let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in (* (try *) let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in @@ -890,7 +906,8 @@ let gotoBottom (cgi : Netcgi.cgi_activation) = cgi#out_channel#commit_work() ;; -let gotoTop (cgi : Netcgi.cgi_activation) = +let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in prerr_endline "executing goto Top"; (try @@ -926,7 +943,8 @@ let gotoTop (cgi : Netcgi.cgi_activation) = cgi#out_channel#commit_work() ;; -let retract (cgi : Netcgi.cgi_activation) = +let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in @@ -970,7 +988,8 @@ let retract (cgi : Netcgi.cgi_activation) = ;; -let viewLib (cgi : Netcgi.cgi_activation) = +let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in @@ -1009,7 +1028,8 @@ let viewLib (cgi : Netcgi.cgi_activation) = ;; -let resetLib (cgi : Netcgi.cgi_activation) = +let resetLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in MatitaAuthentication.reset (); cgi # set_header ~cache:`No_cache diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index 068b30d70..cd25cd15a 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -644,7 +644,7 @@ function advOneStep(xml) { matita.disambMode = true; updateSide(); - throw "Stop"; + throw "Wait"; } else if (is_defined(disamberr)) { // must be fixed in a daemon: it makes sense to return a @@ -655,7 +655,7 @@ function advOneStep(xml) { matita.disambMode = true; next_cp(0); } - throw "Stop"; + throw "Wait"; } else { var error = xml.getElementsByTagName("error")[0]; @@ -678,9 +678,11 @@ function advanceForm1() debug("advance failed"); } } catch (e) { - // nothing to do + if (e == "Stop") + resume(); + else + pause(); }; - resume(); }; pause(); callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape()); @@ -794,7 +796,7 @@ function next_cp(curcp) { var tryagainbutton = document.createElement("input"); tryagainbutton.setAttribute("type","button"); if (new_curcp > 0) { - tryagainbutton.setAttribute("value","Try something else"); + tryagainbutton.setAttribute("value","None of the above"); } else { tryagainbutton.setAttribute("value","Restart"); } @@ -844,7 +846,7 @@ function show_failures() { cancelbutton.setAttribute("onclick","cancel_disambiguate()"); var backbutton = document.createElement("input"); backbutton.setAttribute("type","button"); - backbutton.setAttribute("value","<< Back"); + backbutton.setAttribute("value","<< Go back"); backbutton.setAttribute("onclick","next_cp(" + cpno + ")"); disambcell.appendChild(backbutton); @@ -1056,7 +1058,11 @@ function gotoPos(offset) } catch (er) { init_autotraces(); populate_goalarray(metasenv); - resume(); + if (er == "Stop") + resume(); + else + pause(); + } } else { init_autotraces();