...

diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml
index dc4534c845f332fdc0679113bf520a6badc2a015..82037a1d6a69e8452a194e668eebfc2f1f348b8a 100644 (file)
--- a/matitaB/components/content_pres/cicNotationParser.ml
+++ b/matitaB/components/content_pres/cicNotationParser.ml
@@ -108,7 +108,7 @@ let add_symbol_to_grammar_explicit level2_ast_grammar
           ;Gramext.Stoken ("ATAGEND","")],
           (Gramext.action (fun _ uridesc _ _ _ loc -> (Some uridesc),loc))
         ]]];
-  prerr_endline ("adding to grammar symbol " ^ s);
+(*  prerr_endline ("adding to grammar symbol " ^ s); *)
   (s,entry)::sym_table
  
 

diff --git a/matitaB/components/content_pres/cicNotationPres.ml b/matitaB/components/content_pres/cicNotationPres.ml
index 6bcec8edd4d722062d71f986a19a3edd7e069354..7f1470f76d8f44935ec8a9d1ff1c192a6a8acaf5 100644 (file)
--- a/matitaB/components/content_pres/cicNotationPres.ml
+++ b/matitaB/components/content_pres/cicNotationPres.ml
@@ -87,8 +87,8 @@ let box_of spec attrs children =
            children
        in
         let attrs' =
-         (if spacing then RenderingAttrs.spacing_attributes `BoxML else [])
-          @ (if indent then RenderingAttrs.indent_attributes `BoxML else [])
+          (if spacing then [None, "spacing", "0.5em"] else [])
+          @ (if indent then [None, "indent", "0.5em"] else []) 
           @ attrs
         in
           match kind with
@@ -103,7 +103,17 @@ let render status ?(prec=(-1)) =
     | A.AttributedTerm _ ->
         aux_attributes [] ""  prec t
     | A.Num (literal, _) -> Box.Text ([], literal)
-    | A.Symbol (literal, _) -> Box.Text ([], literal)
+    | A.Symbol (literal, Some (None,desc)) -> 
+        let txt = "<A title=\"" ^ desc ^ "\">" ^ literal ^ "</A>" in 
+                    Box.Text ([], to_unicode txt)
+    | A.Symbol (literal, Some (Some u,desc)) -> 
+        let txt = 
+         "<A href=\"" ^ u ^ "\" title=\"" ^ desc ^ "\">" ^ literal ^ "</A>" in
+        Box.Text ([], to_unicode txt)
+    | A.Symbol (literal, _) -> Box.Text ([], to_unicode literal)
+    | A.Ident (literal, `Uri u) ->
+        let txt = "<A href=\"" ^ u ^ "\">" ^ literal ^ "</A>" in 
+        Box.Text ([], to_unicode txt)
     | A.Ident (literal, _) -> Box.Text ([], to_unicode literal)
     | A.Meta(n, l) ->
         let local_context =
@@ -194,17 +204,47 @@ let render status ?(prec=(-1)) =
     | A.InfRule (t1, t2, t3) -> assert false
     | A.Sqrt t -> assert false
     | A.Root (t1, t2) -> assert false
-    | A.Box (a, terms) -> 
-        let children = List.map (aux prec) terms in
-        Box.H([],children)
+    | A.Box ((_,spacing,_) as kind, terms) ->
+        let children =
+          aux_children spacing prec
+            (NotationUtil.ungroup terms)
+        in
+        box_of kind attrs children
     | A.Mstyle (l,terms) -> assert false
     | A.Mpadded (l,terms) -> assert false
     | A.Maction alternatives -> 
          toggle_action (List.map invoke_reinit alternatives)
     | A.Group terms -> assert false 
-    | A.Break -> Box.Space [] 
+    | A.Break -> Box.Space []
+  and aux_children spacing prec terms =
+    let find_clusters =
+      let rec aux_list first clusters acc =
+        function
+            [] when acc = [] -> List.rev clusters
+          | [] -> aux_list first (List.rev acc :: clusters) [] []
+          | (A.Layout A.Break) :: tl when acc = [] ->
+              aux_list first clusters [] tl
+          | (A.Layout A.Break) :: tl ->
+              aux_list first (List.rev acc :: clusters) [] tl
+          | [hd] ->
+                aux_list false clusters
+                  (aux prec hd :: acc) []
+          | hd :: tl ->
+                aux_list false clusters
+                  (aux prec hd :: acc) tl
+      in
+        aux_list true [] []
+    in
+    let boxify_pres =
+      function
+          [t] -> t
+        | tl -> box_of (A.H, spacing, false) [] tl
+    in
+      List.map boxify_pres (find_clusters terms) 
   in
-  aux prec
+  (fun t ->
+          prerr_endline ("ast:\n" ^ (NotationPp.pp_term status t));
+  aux prec t)
 
 (* let render_to_boxml id_to_uri t =
   let xml_stream = print_box (box_of_mpres (render id_to_uri t)) in
@@ -221,14 +261,15 @@ let render_context_entry status name = function
               render status (TermContentPres.pp_ast status t)])
 
 let render_context status context =
-  Box.V ([],
+  Box.V ([], 
+         Box.Space [None, "width", "0.5em"]:: 
         List.map 
           (fun (name,entry) -> 
              render_context_entry status (to_unicode name) entry) context)
 
 let render_sequent status (i,context,ty) =
   Box.V ([],
-        [render_context status context;
+        [render_context status (List.rev context);
          Box.Ink [None,"width","4cm"; None,"height","2px"];
           render status (TermContentPres.pp_ast status ty)])
          

diff --git a/matitaB/components/content_pres/termContentPres.ml b/matitaB/components/content_pres/termContentPres.ml
index 2b9bc650fcc9ec7b590e48e2ea27c25c5f0841d8..d51e4bf02ca392d08571431af6d41bdddcf8d4af 100644 (file)
--- a/matitaB/components/content_pres/termContentPres.ml
+++ b/matitaB/components/content_pres/termContentPres.ml
@@ -472,7 +472,8 @@ let rec pp_ast1 status term =
   let ast_env_of_env 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 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')
@@ -489,6 +490,9 @@ let rec pp_ast1 status term =
             with Not_found -> assert false
           in
           instantiate21 idrefs (ast_env_of_env env) l1)
+  in
+  prerr_endline ("### pattern matching finished: " ^ NotationPp.pp_term status res);
+  res
 
 let load_patterns21 status t =
   set_compiled21 status (lazy (Content2presMatcher.Matcher21.compiler t))

diff --git a/matitaB/components/ng_cic_content/interpretations.ml b/matitaB/components/ng_cic_content/interpretations.ml
index 226eecdfde7800c7d06bbd2868acd7c215398902..75f46943052cc16868f64d102fd5255b279042b0 100644 (file)
--- a/matitaB/components/ng_cic_content/interpretations.ml
+++ b/matitaB/components/ng_cic_content/interpretations.ml
@@ -89,7 +89,7 @@ let level_of_uri u =
 let find_level2_patterns32 status pid =
  IntMap.find pid status#interp_db.level2_patterns32
 
-let instantiate32 env symbol args =
+let instantiate32 env symbol dsc args =
   let rec instantiate_arg = function
     | Ast.IdentArg (n, name) ->
         let t = 
@@ -112,7 +112,7 @@ let instantiate32 env symbol args =
         in
         add_lambda t (n - count_lambda t)
   in
-  let head = Ast.Symbol (symbol, None) in
+  let head = Ast.Symbol (symbol, Some (None, dsc)) in
   if args = [] then head
   else Ast.Appl (head :: List.map instantiate_arg args)
 
@@ -338,12 +338,12 @@ let rec nast_of_cic1 status ~output_type ~metasenv ~subst ~context term =
             term
         ) env
       in
-      let _, symbol, args, _ =
+      let dsc, symbol, args, _ =
         try
          find_level2_patterns32 status pid
         with Not_found -> assert false
       in
-      instantiate32 env symbol args 
+      instantiate32 env symbol dsc args 
 ;;
 
 let nmap_context0 status ~metasenv ~subst context =

diff --git a/matitaB/matita/applyTransformation.ml b/matitaB/matita/applyTransformation.ml
index a911742b05e980b810aaf8f7b74db4078ea197a3..5db35244e397e1e4020403219b4d246e8a95fc04 100644 (file)
--- a/matitaB/matita/applyTransformation.ml
+++ b/matitaB/matita/applyTransformation.ml
@@ -101,7 +101,7 @@ class status =
   method ppmetasenv ~subst metasenv =
    String.concat "\n"
     (List.map
-      (fun m -> ntxt_of_cic_sequent ~map_unicode_to_tex:true 20 self
+      (fun m -> ntxt_of_cic_sequent ~map_unicode_to_tex:true 50 self
         ~metasenv ~subst m) metasenv)
 (*
   method ppobj obj =

diff --git a/matitaB/matita/cicMathView.ml b/matitaB/matita/cicMathView.ml
index 9f1a004584017252026ddc9972bf50a805f93b26..effa760014fe0bb87ff4734c733f92d3b03022c1 100644 (file)
--- a/matitaB/matita/cicMathView.ml
+++ b/matitaB/matita/cicMathView.ml
@@ -637,7 +637,7 @@ object (self)
     let sequent = List.assoc metano metasenv in
     let txt =
      ApplyTransformation.ntxt_of_cic_sequent
-      ~map_unicode_to_tex:false 20 status ~metasenv ~subst (metano,sequent)
+      ~map_unicode_to_tex:false 50 status ~metasenv ~subst (metano,sequent)
     in
     (* MATITA 1.0 if BuildTimeConf.debug then begin
       let name =