X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaMathView.ml;h=b8dd3f1bdcb5bb2d5e0f01428aaf08306ac06fec;hb=f39bfe067b475f99d3da6c1c62b101e17819c3a4;hp=ee49267fe3c57d1579fb2924dd07dc4c7e1c0150;hpb=394177fef9a7a158a527077b69928b0a9818bce8;p=helm.git

diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml
index ee49267fe..b8dd3f1bd 100644
--- a/matita/matitaMathView.ml
+++ b/matita/matitaMathView.ml
@@ -252,7 +252,7 @@ object (self)
    match self#get_term_by_id cic_info id with
    | SelTerm (t, father_hyp) ->
        let sequent = self#sequent_of_id ~paste_kind:`Pattern id in
-       let text = self#string_of_cic_sequent sequent in
+       let text = self#string_of_cic_sequent ~output_type:`Pattern sequent in
        (match father_hyp with
        | None -> None, [], Some text
        | Some hyp_name -> None, [ hyp_name, text ], None)
@@ -264,7 +264,7 @@ object (self)
    match self#get_term_by_id cic_info id with
    | SelTerm (t, father_hyp) ->
        let sequent = self#sequent_of_id ~paste_kind:`Term id in
-       let text = self#string_of_cic_sequent sequent in
+       let text = self#string_of_cic_sequent ~output_type:`Term sequent in
        text
    | SelHyp (hyp_name, _ctxt) -> hyp_name
 
@@ -303,9 +303,11 @@ object (self)
         "\n" ^
         GrafiteAstPp.pp_executable ~term_pp:(fun s -> s)
           ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
-          (GrafiteAst.Tactical (loc,
-            GrafiteAst.Tactic (loc, GrafiteAst.Reduce (loc, kind, pat)),
-            Some (GrafiteAst.Semicolon loc))) in
+          ~map_unicode_to_tex:(Helm_registry.get_bool
+            "matita.paste_unicode_as_tex")
+          (GrafiteAst.Tactic (loc,
+            Some (GrafiteAst.Reduce (loc, kind, pat)),
+            GrafiteAst.Semicolon loc)) in
       (MatitaScript.current ())#advance ~statement () in
     connect_menu_item copy gui#copy;
     connect_menu_item normalize (reduction_action `Normalize);
@@ -434,41 +436,37 @@ object (self)
           let tactic_text_pattern =  self#tactic_text_pattern_of_node node in
           GrafiteAstPp.pp_tactic_pattern
             ~term_pp:(fun s -> s) ~lazy_term_pp:(fun _ -> assert false)
+            ~map_unicode_to_tex:(Helm_registry.get_bool
+              "matita.paste_unicode_as_tex")
             tactic_text_pattern
       | `Term -> self#tactic_text_of_node node
     else string_of_dom_node node
 
-  method private string_of_cic_sequent cic_sequent =
+  method private string_of_cic_sequent ~output_type cic_sequent =
     let script = MatitaScript.current () in
     let metasenv =
       if script#onGoingProof () then script#proofMetasenv else [] in
-    (*
-    let _, (acic_sequent, _, _, ids_to_inner_sorts, _) =
-      Cic2acic.asequent_of_sequent metasenv cic_sequent in
-    let _, _, _, annterm = acic_sequent in
-    let ast, ids_to_uris =
-      TermAcicContent.ast_of_acic ids_to_inner_sorts annterm in
-    let pped_ast = TermContentPres.pp_ast ast in
-    let markup = CicNotationPres.render ids_to_uris pped_ast in
-    BoxPp.render_to_string text_width markup
-    *)
-    ApplyTransformation.txt_of_cic_sequent_conclusion 
-      text_width metasenv cic_sequent
-
-  method private pattern_of term context unsh_sequent =
-    let context_len = List.length context in
+    let map_unicode_to_tex =
+      Helm_registry.get_bool "matita.paste_unicode_as_tex" in
+    ApplyTransformation.txt_of_cic_sequent_conclusion ~map_unicode_to_tex
+     ~output_type text_width metasenv cic_sequent
+
+  method private pattern_of term father_hyp unsh_sequent =
     let _, unsh_context, conclusion = unsh_sequent in
-    try
-      (match
-        List.nth unsh_context (List.length unsh_context - context_len - 1)
-      with
-      | None -> assert false (* can't select a restricted hypothesis *)
-      | Some (name, Cic.Decl ty) ->
-          ProofEngineHelpers.pattern_of ~term:ty [term]
-      | Some (name, Cic.Def (bo, _)) ->
-          ProofEngineHelpers.pattern_of ~term:bo [term])
-    with Failure _ | Invalid_argument _ ->
-      ProofEngineHelpers.pattern_of ~term:conclusion [term]
+    let where =
+     match father_hyp with
+        None -> conclusion
+      | Some name ->
+         let rec aux =
+          function
+             [] -> assert false
+           | Some (Cic.Name name', Cic.Decl ty)::_ when name' = name -> ty
+           | Some (Cic.Name name', Cic.Def (bo,_))::_ when name' = name-> bo
+           | _::tl -> aux tl
+         in
+          aux unsh_context
+    in
+     ProofEngineHelpers.pattern_of ~term:where [term]
 
   method private get_cic_info id =
     match self#cic_info with
@@ -482,14 +480,17 @@ object (self)
     let cic_info, unsh_sequent = self#get_cic_info id in
     let cic_sequent =
       match self#get_term_by_id cic_info id with
-      | SelTerm (t, _father_hyp) ->
+      | SelTerm (t, father_hyp) ->
+(*
+IDIOTA: PRIMA SI FA LA LOCATE, POI LA PATTERN_OF. MEGLIO UN'UNICA pattern_of CHE PRENDA IN INPUT UN TERMINE E UN SEQUENTE. PER IL MOMENTO RISOLVO USANDO LA father_hyp PER RITROVARE L'IPOTESI PERDUTA
+*)
           let occurrences =
             ProofEngineHelpers.locate_in_conjecture t unsh_sequent in
           (match occurrences with
           | [ context, _t ] ->
               (match paste_kind with
               | `Term -> ~-1, context, t
-              | `Pattern -> ~-1, [], self#pattern_of t context unsh_sequent)
+              | `Pattern -> ~-1, [], self#pattern_of t father_hyp unsh_sequent)
           | _ ->
               HLog.error (sprintf "found %d occurrences while 1 was expected"
                 (List.length occurrences));
@@ -648,7 +649,9 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       _metasenv <- []; 
       self#script#setGoal None
 
-    method load_sequents { proof = (_,metasenv,_,_) as proof; stack = stack } =
+    method load_sequents 
+      { proof = (_,metasenv,_subst,_,_, _) as proof; stack = stack } 
+    =
       _metasenv <- metasenv;
       pages <- 0;
       let win goal_switch =
@@ -928,8 +931,12 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
         match self#currentCicUri with
         | Some uri -> self#load (`Metadata (`Deps (`Back, uri)))
         | None -> ());
+      (* remove hbugs *)
+      (*
       connect_menu_item win#hBugsTutorsMenuItem (fun () ->
         self#load (`HBugs `Tutors));
+      *)
+      win#hBugsTutorsMenuItem#misc#hide ();
       connect_menu_item win#browserUrlMenuItem (fun () ->
         win#browserUri#entry#misc#grab_focus ());
 
@@ -1090,13 +1097,13 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     method private home () =
       self#_showMath;
       match self#script#grafite_status.proof_status with
-      | Proof  (uri, metasenv, bo, ty) ->
+      | Proof  (uri, metasenv, _subst, bo, ty, attrs) ->
           let name = UriManager.name_of_uri (HExtlib.unopt uri) in
-          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
+          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
           self#_loadObj obj
-      | Incomplete_proof { proof = (uri, metasenv, bo, ty) } ->
+      | Incomplete_proof { proof = (uri, metasenv, _subst, bo, ty, attrs) } ->
           let name = UriManager.name_of_uri (HExtlib.unopt uri) in
-          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
+          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
           self#_loadObj obj
       | _ -> self#blank ()
 
@@ -1108,7 +1115,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#_loadObj obj
       
     method private _loadDir dir = 
-      let content = Http_getter.ls dir in
+      let content = Http_getter.ls ~local:false dir in
       let l =
         List.fast_sort
           Pervasives.compare