From 1b67bd4dfa12ef25b8fa63884c71893b961db27d Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Mon, 23 May 2011 15:13:38 +0000 Subject: [PATCH] Added support for hyperlinks in the goal view of the web interface. --- .../components/METAS/meta.helm-content.src | 2 +- matitaB/components/content/.depend | 6 ++- matitaB/components/content/notationEnv.ml | 15 ++++++++ matitaB/components/content/notationPp.ml | 14 +++---- matitaB/components/content/notationPt.ml | 6 +-- matitaB/components/content/notationUtil.ml | 38 ++++++++++++++----- matitaB/components/content/notationUtil.mli | 2 + matitaB/components/content_pres/.depend | 6 +-- matitaB/components/content_pres/boxPp.ml | 25 +++++++++++- .../content_pres/cicNotationParser.ml | 24 ++++++------ .../content_pres/cicNotationPres.ml | 36 ++++++++++-------- .../content_pres/content2presMatcher.ml | 1 + .../content_pres/termContentPres.ml | 38 ++++++++++++------- matitaB/matita/matitadaemon.ml | 14 ++++--- 14 files changed, 153 insertions(+), 74 deletions(-) diff --git a/matitaB/components/METAS/meta.helm-content.src b/matitaB/components/METAS/meta.helm-content.src index 6973a54d9..8a7fbe668 100644 --- a/matitaB/components/METAS/meta.helm-content.src +++ b/matitaB/components/METAS/meta.helm-content.src @@ -1,4 +1,4 @@ -requires="helm-library helm-ng_kernel" +requires="helm-library helm-ng_kernel helm-syntax_extensions" version="0.0.1" archive(byte)="content.cma" archive(native)="content.cmxa" diff --git a/matitaB/components/content/.depend b/matitaB/components/content/.depend index 297edefdb..6d0eb1f22 100644 --- a/matitaB/components/content/.depend +++ b/matitaB/components/content/.depend @@ -7,5 +7,7 @@ notationUtil.cmo: notationPt.cmo notationUtil.cmi notationUtil.cmx: notationPt.cmx notationUtil.cmi notationEnv.cmo: notationUtil.cmi notationPt.cmo notationEnv.cmi notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi -notationPp.cmo: notationPt.cmo notationEnv.cmi notationPp.cmi -notationPp.cmx: notationPt.cmx notationEnv.cmx notationPp.cmi +notationPp.cmo: notationUtil.cmi notationPt.cmo notationEnv.cmi \ + notationPp.cmi +notationPp.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmx \ + notationPp.cmi diff --git a/matitaB/components/content/notationEnv.ml b/matitaB/components/content/notationEnv.ml index 986c9b63c..eb85ec038 100644 --- a/matitaB/components/content/notationEnv.ml +++ b/matitaB/components/content/notationEnv.ml @@ -54,6 +54,21 @@ type declaration = string * value_type type binding = string * (value_type * value) type t = binding list +(* let rec pp_value = function + | TermValue t -> "T#" ^ NotationPp.pp_term (new NCicPp.status) t + | StringValue (Ident i) -> "I#" ^ i + | StringValue (Var v) -> "V#" ^ v + | NumValue n -> "N#" ^ n + | OptValue None -> "O#None" + | OptValue (Some v) -> "O#" ^ pp_value v + | ListValue vl -> "L#[" ^ (String.concat ";" (List.map pp_value vl)) ^ "]" + | DisambiguationValue _ -> "D#" + +let pp_binding = function + | s, (ty,v) -> Printf.sprintf "{ %s := %s : %s }" s (pp_value v) "..." + +let pp_env e = String.concat " " (List.map pp_binding e) *) + let lookup env name = try List.assoc name env diff --git a/matitaB/components/content/notationPp.ml b/matitaB/components/content/notationPp.ml index 082a5ddf8..50ccb16b4 100644 --- a/matitaB/components/content/notationPp.ml +++ b/matitaB/components/content/notationPp.ml @@ -45,14 +45,12 @@ let pp_binder = function let pp_literal = if debug_printing then (function (* debugging version *) - | `Symbol s -> sprintf "symbol(%s)" s - | `Keyword s -> sprintf "keyword(%s)" s - | `Number s -> sprintf "number(%s)" s) - else - (function - | `Symbol s - | `Keyword s - | `Number s -> s) + | `Symbol _ as t -> + sprintf "symbol(%s)" (NotationUtil.string_of_literal t) + | `Keyword _ as t -> + sprintf "keyword(%s)" (NotationUtil.string_of_literal t) + | `Number _ as t -> sprintf "number(%s)" (NotationUtil.string_of_literal t)) + else NotationUtil.string_of_literal let pp_pos = function diff --git a/matitaB/components/content/notationPt.ml b/matitaB/components/content/notationPt.ml index 2c94ec356..b624c9a86 100644 --- a/matitaB/components/content/notationPt.ml +++ b/matitaB/components/content/notationPt.ml @@ -51,9 +51,9 @@ type term_attribute = ] type literal = - [ `Symbol of string - | `Keyword of string - | `Number of string + [ `Symbol of string * (string option * string option) + | `Keyword of string * (string option * string option) + | `Number of string * (string option * string option) ] type case_indtype = string * href option diff --git a/matitaB/components/content/notationUtil.ml b/matitaB/components/content/notationUtil.ml index eeb1cd5c6..d047eb58e 100644 --- a/matitaB/components/content/notationUtil.ml +++ b/matitaB/components/content/notationUtil.ml @@ -27,7 +27,8 @@ module Ast = NotationPt -let visit_ast ?(special_k = fun _ -> assert false) +let visit_ast ?(special_k = fun _ -> assert false) + ?(clear_interpretation= false) ?(map_xref_option= fun x -> x) ?(map_case_indty= fun x -> x) ?(map_case_outtype= fun k x -> match x with None -> None | Some x -> Some (k x)) @@ -58,13 +59,16 @@ let visit_ast ?(special_k = fun _ -> assert false) | Ast.Literal _ | Ast.Magic _ | Ast.Variable _) as t -> special_k t - | (Ast.Ident _ + | Ast.Ident (id,_) when clear_interpretation -> Ast.Ident (id,`Ambiguous) + | Ast.Symbol (s,_) when clear_interpretation -> Ast.Symbol (s,None) + | Ast.Num (n,_) when clear_interpretation -> Ast.Num (n,None) + | ( Ast.Ident _ + | Ast.Symbol _ + | Ast.Num _ | Ast.NRef _ | Ast.NCic _ | Ast.Implicit _ - | Ast.Num _ | Ast.Sort _ - | Ast.Symbol _ | Ast.UserInput) as t -> t and aux_opt = function | None -> None @@ -153,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 @@ -175,8 +179,7 @@ let rec strip_attributes t = let rec get_idrefs = function - | Ast.AttributedTerm (`IdRef id, t) -> id :: get_idrefs t - | Ast.AttributedTerm (_, t) -> get_idrefs t + | Ast.Symbol (_,Some (_,desc)) -> [desc] | _ -> [] let meta_names_of_term term = @@ -271,10 +274,25 @@ let ncombine ll = done; List.rev !lists +let href s = function + | None, None -> s + | Some u, None -> "" ^ s ^ "" + | None, Some desc -> + "" ^ s ^ "" + | Some u, Some desc -> + "" ^ s ^ "" + let string_of_literal = function - | `Symbol s - | `Keyword s - | `Number s -> s + | `Symbol (s,x) + | `Keyword (s,x) + | `Number (s,x) -> href s x + +let html_of_literal = function + | `Symbol (s,x) + | `Keyword (s,x) + | `Number (s,x) -> + href (Netencoding.Html.encode ~in_enc:`Enc_utf8 () + (Utf8Macro.unicode_of_tex s)) x let boxify = function | [ a ] -> a diff --git a/matitaB/components/content/notationUtil.mli b/matitaB/components/content/notationUtil.mli index ac291a2ce..981030d49 100644 --- a/matitaB/components/content/notationUtil.mli +++ b/matitaB/components/content/notationUtil.mli @@ -33,6 +33,7 @@ val keywords_of_term: NotationPt.term -> string list val visit_ast: ?special_k:(NotationPt.term -> NotationPt.term) -> + ?clear_interpretation:bool -> ?map_xref_option:(NotationPt.href option -> NotationPt.href option) -> ?map_case_indty:(NotationPt.case_indtype option -> NotationPt.case_indtype option) -> @@ -67,6 +68,7 @@ val get_idrefs: NotationPt.term -> string list val ncombine: 'a list list -> 'a list list val string_of_literal: NotationPt.literal -> string +val html_of_literal: NotationPt.literal -> string val dress: sep:'a -> 'a list -> 'a list val dressn: sep:'a list -> 'a list -> 'a list diff --git a/matitaB/components/content_pres/.depend b/matitaB/components/content_pres/.depend index bcbd3cae2..3a1c6036d 100644 --- a/matitaB/components/content_pres/.depend +++ b/matitaB/components/content_pres/.depend @@ -2,10 +2,10 @@ cicNotationLexer.cmi: smallLexer.cmi: cicNotationParser.cmi: box.cmi: +content2presMatcher.cmi: termContentPres.cmi: cicNotationParser.cmi boxPp.cmi: cicNotationPres.cmi cicNotationPres.cmi: termContentPres.cmi box.cmi -content2presMatcher.cmi: cicNotationLexer.cmo: cicNotationLexer.cmi cicNotationLexer.cmx: cicNotationLexer.cmi smallLexer.cmo: smallLexer.cmi @@ -14,6 +14,8 @@ cicNotationParser.cmo: cicNotationLexer.cmi cicNotationParser.cmi cicNotationParser.cmx: cicNotationLexer.cmx cicNotationParser.cmi box.cmo: box.cmi box.cmx: box.cmi +content2presMatcher.cmo: content2presMatcher.cmi +content2presMatcher.cmx: content2presMatcher.cmi termContentPres.cmo: content2presMatcher.cmi cicNotationParser.cmi \ termContentPres.cmi termContentPres.cmx: content2presMatcher.cmx cicNotationParser.cmx \ @@ -22,5 +24,3 @@ boxPp.cmo: box.cmi boxPp.cmi boxPp.cmx: box.cmx boxPp.cmi cicNotationPres.cmo: termContentPres.cmi box.cmi cicNotationPres.cmi cicNotationPres.cmx: termContentPres.cmx box.cmx cicNotationPres.cmi -content2presMatcher.cmo: content2presMatcher.cmi -content2presMatcher.cmx: content2presMatcher.cmi diff --git a/matitaB/components/content_pres/boxPp.ml b/matitaB/components/content_pres/boxPp.ml index 9511de631..af11da811 100644 --- a/matitaB/components/content_pres/boxPp.ml +++ b/matitaB/components/content_pres/boxPp.ml @@ -104,10 +104,33 @@ let fixed_rendering s = let render_to_strings ~map_unicode_to_tex choose_action size markup = prerr_endline ("render size is " ^ string_of_int size); + let add_markup attr txt = + let txt = Netencoding.Html.encode ~in_enc:`Enc_utf8 () txt in + let value_of_attr (_,_,v) = v in + let title = + try Some (value_of_attr (List.find (fun (_,t,_) -> t = "title") attr)) + with _ -> None in + let href = + try Some (value_of_attr (List.find (fun (_,t,_) -> t = "href") attr)) + with _ -> None in + match title,href with + | None,None -> txt + | None,Some u -> "" ^ txt ^ "" + | Some t, Some u -> + "" ^ txt ^ "" + | Some t, None -> + let u = "cic:/fakeuri.con" in + "" ^ txt ^ "" + in + let max_size = max_int in let rec aux_box = function - | Box.Text (_, t) -> fixed_rendering t + | Box.Text (attr, t) -> + fun x -> + (match fixed_rendering t x with + | len, [txt] -> len, [add_markup attr txt] + | _ -> assert false) | Box.Space _ -> fixed_rendering string_space | Box.Ink _ -> fixed_rendering string_ink | Box.Action (_, []) -> assert false diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml index 82037a1d6..7361bf599 100644 --- a/matitaB/components/content_pres/cicNotationParser.ml +++ b/matitaB/components/content_pres/cicNotationParser.ml @@ -157,9 +157,9 @@ let gram_term status = function let gram_of_literal status = function - | `Symbol s -> gram_symbol status s - | `Keyword s -> gram_keyword s - | `Number s -> gram_number s + | `Symbol (s,_) -> gram_symbol status s + | `Keyword (s,_) -> gram_keyword s + | `Number (s,_) -> gram_number s let make_action status action bindings = let rec aux (vl : NotationEnv.t) = @@ -226,9 +226,9 @@ let update_sym_grammar status pattern = assert false and aux_literal status = function - | `Symbol s -> add_symbol_to_grammar status s - | `Keyword s -> status - | `Number s -> status + | `Symbol (s,_) -> add_symbol_to_grammar status s + | `Keyword _ -> 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 @@ -273,11 +273,11 @@ let extract_term_production status pattern = assert false and aux_literal = function - | `Symbol s -> [NoBinding, gram_symbol status s] - | `Keyword s -> + | `Symbol (s,_) -> [NoBinding, gram_symbol status s] + | `Keyword (s,_) -> (* assumption: s will be registered as a keyword with the lexer *) [NoBinding, gram_keyword s] - | `Number s -> [NoBinding, gram_number s] + | `Number (s,_) -> [NoBinding, 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 @@ -528,9 +528,9 @@ EXTEND fun l -> List.map (fun x -> x l) p ] ]; literal: [ - [ s = SYMBOL -> `Symbol s - | k = QKEYWORD -> `Keyword k - | n = NUMBER -> `Number n + [ s = SYMBOL -> `Symbol (s, (None,None)) + | k = QKEYWORD -> `Keyword (k, (None,None)) + | n = NUMBER -> `Number (n,(None,None)) ] ]; sep: [ [ "sep"; sep = literal -> sep ] ]; diff --git a/matitaB/components/content_pres/cicNotationPres.ml b/matitaB/components/content_pres/cicNotationPres.ml index 7f1470f76..e0ca07b56 100644 --- a/matitaB/components/content_pres/cicNotationPres.ml +++ b/matitaB/components/content_pres/cicNotationPres.ml @@ -103,17 +103,19 @@ let render status ?(prec=(-1)) = | A.AttributedTerm _ -> aux_attributes [] "" prec t | A.Num (literal, _) -> Box.Text ([], literal) - | A.Symbol (literal, Some (None,desc)) -> - let txt = "" ^ literal ^ "" in - Box.Text ([], to_unicode txt) + | A.Symbol (literal, Some (None,desc)) -> + let literal = to_unicode literal in + let attr = [ None, "title", desc ] in + Box.Text (attr, literal) | A.Symbol (literal, Some (Some u,desc)) -> - let txt = - "" ^ literal ^ "" in - Box.Text ([], to_unicode txt) + let literal = to_unicode literal in + let attr = [ None, "title", desc; None, "href", u ] in + Box.Text (attr, literal) | A.Symbol (literal, _) -> Box.Text ([], to_unicode literal) | A.Ident (literal, `Uri u) -> - let txt = "" ^ literal ^ "" in - Box.Text ([], to_unicode txt) + let attr = [ None, "href", u ] in + let literal = to_unicode literal in + Box.Text (attr,literal) | A.Ident (literal, _) -> Box.Text ([], to_unicode literal) | A.Meta(n, l) -> let local_context = @@ -128,7 +130,17 @@ let render status ?(prec=(-1)) = Box.H ([], (Box.Text ([], "?"^string_of_int n):: (if (l <> []) then [Box.H ([],local_context)] else []))) - | A.Literal l -> aux_literal prec l + | A.Literal (`Symbol (s,x)) + | A.Literal (`Keyword (s,x)) + | A.Literal (`Number (s,x)) -> + let attr = + match x with + | None, None -> [] + | Some u, None -> [ None, "href", u ] + | None, Some d -> [ None, "title", d ] + | Some u, Some d -> [ None, "href", u; None, "title", d ] + in + Box.Text (attr, to_unicode s) | A.UserInput -> Box.Text ([], "%") | A.Layout l -> aux_layout prec l | A.Magic _ @@ -179,12 +191,6 @@ let render status ?(prec=(-1)) = (* prerr_endline (NotationPp.pp_term t); *) aux_attribute t - and aux_literal prec l = - (match l with - | `Symbol s -> Box.Text ([], to_unicode s) - | `Keyword s -> Box.Text ([], to_unicode s) - | `Number s -> Box.Text ([], to_unicode s)) - and aux_layout prec l = let attrs = [] in let invoke' t = aux prec t in diff --git a/matitaB/components/content_pres/content2presMatcher.ml b/matitaB/components/content_pres/content2presMatcher.ml index cf5d66b6a..a7b59aa52 100644 --- a/matitaB/components/content_pres/content2presMatcher.ml +++ b/matitaB/components/content_pres/content2presMatcher.ml @@ -40,6 +40,7 @@ let get_tag term0 = in let rec aux t = NotationUtil.visit_ast + ~clear_interpretation:true ~map_xref_option:(fun _ -> None) ~map_case_indty:(fun _ -> None) ~map_case_outtype:(fun _ _ -> None) diff --git a/matitaB/components/content_pres/termContentPres.ml b/matitaB/components/content_pres/termContentPres.ml index d51e4bf02..8ff5a13f2 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 " ") -let builtin_symbol s = Ast.Literal (`Symbol s) -let keyword k = add_keyword_attrs (Ast.Literal (`Keyword k)) +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 number s = add_xml_attrs (* (RenderingAttrs.number_attributes `MathML) *) () - (Ast.Literal (`Number s)) + (Ast.Literal (`Number (s,(None,None)))) let ident i = add_xml_attrs (* (RenderingAttrs.ident_attributes `MathML) *) () @@ -337,8 +337,8 @@ let set_compiled21 status f = status#set_content_pres_db { status#content_pres_db with compiled21 = Some f } -let add_idrefs = - List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t)) +(* let add_idrefs = + List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t)) *) let instantiate21 idrefs env l1 = let rec subst_singleton pos env = @@ -376,10 +376,14 @@ let instantiate21 idrefs env l1 = [ value ] | Ast.Magic m -> subst_magic pos env m | Ast.Literal l as t -> - let t = add_idrefs idrefs t in - (match l with - | `Keyword k -> [ add_keyword_attrs t ] - | _ -> [ t ]) + (match idrefs with + | [] -> [t] + | 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))) ])) | 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 @@ -470,17 +474,24 @@ let rec pp_ast1 status term = | NotationEnv.DisambiguationValue _ as v -> v in let ast_env_of_env env = + prerr_endline ("### pp_env: " ^ NotationPp.pp_env status env); List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env in - prerr_endline ("### pattern matching from 2 to 1 on term " ^ NotationPp.pp_term status term); +(* prerr_endline ("### pattern matching from 2 to 1 on term " ^ + * NotationPp.pp_term status term); *) let res = match term with | Ast.AttributedTerm (attrs, term') -> Ast.AttributedTerm (attrs, pp_ast1 status term') | _ -> (match get_compiled21 status term with - | None -> pp_ast0 status term (pp_ast1 status) + | None -> (* prerr_endline "### ramo 1"; *) + pp_ast0 status term (pp_ast1 status) | Some (env, ctors, pid) -> + (* prerr_endline "### ramo 2"; + prerr_endline ("### constructors:\n" ^ + (String.concat "\n\n" (List.map (NotationPp.pp_term status) ctors)) ^ + "\n\n### constructors end") *) let idrefs = List.flatten (List.map NotationUtil.get_idrefs ctors) in @@ -491,7 +502,8 @@ let rec pp_ast1 status term = in instantiate21 idrefs (ast_env_of_env env) l1) in - prerr_endline ("### pattern matching finished: " ^ NotationPp.pp_term status res); + (* prerr_endline ("### pattern matching finished: " ^ NotationPp.pp_term + * status res);*) res let load_patterns21 status t = diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 5c58db371..d1a7e2072 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -50,9 +50,10 @@ let advance text (* (?bos=false) *) = let _,_,metasenv,subst,_ = !status#obj in let txt = List.fold_left (fun acc (nmeta,_ as meta) -> - let txt0 = Netencoding.Html.encode ~in_enc:`Enc_utf8 () - (snd (ApplyTransformation.ntxt_of_cic_sequent - ~metasenv ~subst ~map_unicode_to_tex:false 80 !status meta)) in + let txt0 = snd (ApplyTransformation.ntxt_of_cic_sequent + ~metasenv ~subst ~map_unicode_to_tex:false 80 !status + meta) in + prerr_endline ("### txt0 = " ^ txt0); ("Goal ?" ^ (string_of_int nmeta) ^ "\n" ^ txt0)::acc) [] metasenv in @@ -171,9 +172,10 @@ let callback req outchan = let _,_,metasenv,subst,_ = !status#obj in let txt = List.fold_left (fun acc (nmeta,_ as meta) -> - let txt0 = Netencoding.Html.encode ~in_enc:`Enc_utf8 () - (snd (ApplyTransformation.ntxt_of_cic_sequent - ~metasenv ~subst ~map_unicode_to_tex:false 80 !status meta)) in + let txt0 = snd (ApplyTransformation.ntxt_of_cic_sequent + ~metasenv ~subst ~map_unicode_to_tex:false 80 !status + meta) in + prerr_endline ("### txt0 = " ^ txt0); ("Goal ?" ^ (string_of_int nmeta) ^ "\n" ^ txt0)::acc) [] metasenv in -- 2.39.2