Compilation fix

diff --git a/matitaB/components/content/.depend b/matitaB/components/content/.depend
index f4b4f30379ca932caaa4dccdf4465f929003f28c..297edefdbb5364bc053bad5253083b8922687c75 100644 (file)
--- a/matitaB/components/content/.depend
+++ b/matitaB/components/content/.depend
@@ -1,11 +1,8 @@
-content.cmi: 
 notationUtil.cmi: notationPt.cmo 
 notationEnv.cmi: notationPt.cmo 
 notationPp.cmi: notationPt.cmo notationEnv.cmi 
 notationPt.cmo: 
 notationPt.cmx: 
-content.cmo: content.cmi 
-content.cmx: content.cmi 
 notationUtil.cmo: notationPt.cmo notationUtil.cmi 
 notationUtil.cmx: notationPt.cmx notationUtil.cmi 
 notationEnv.cmo: notationUtil.cmi notationPt.cmo notationEnv.cmi 

diff --git a/matitaB/components/content_pres/Makefile b/matitaB/components/content_pres/Makefile
index 658d8d354d62465e5ef717dc723034e8ae4abad6..9d192c5b936e6d6ac6f12310cefa4d1a8f45a72b 100644 (file)
--- a/matitaB/components/content_pres/Makefile
+++ b/matitaB/components/content_pres/Makefile
@@ -6,10 +6,10 @@ INTERFACE_FILES =              \
        smallLexer.mli   \
        cicNotationParser.mli    \
        box.mli                  \
+       content2presMatcher.mli  \
        termContentPres.mli      \
        boxPp.mli                \
        cicNotationPres.mli      \
-       content2presMatcher.mli  \
        $(NULL)
 IMPLEMENTATION_FILES =          \
        $(INTERFACE_FILES:%.mli=%.ml) \

diff --git a/matitaB/components/content_pres/box.ml b/matitaB/components/content_pres/box.ml
index 6e5bb4d922910fee54e5357ee41ab9c6226ac567..74cc844e6fc0b9b2a73a20064717c35002f1326a 100644 (file)
--- a/matitaB/components/content_pres/box.ml
+++ b/matitaB/components/content_pres/box.ml
@@ -110,7 +110,7 @@ let b_text a b = Text(a,b)
 let b_object b = Object ([],b)
 let b_indent = indent
 let b_space = Space [None, "width", "0.5em"]
-let b_kw = b_text (RenderingAttrs.object_keyword_attributes `BoxML)
+(* let b_kw = b_text (RenderingAttrs.object_keyword_attributes `BoxML) *)
 let b_toggle items = Action ([ None, "type", "toggle"], items)
 
 let pp_attr attr =

diff --git a/matitaB/components/content_pres/box.mli b/matitaB/components/content_pres/box.mli
index e7c2588ebade764d308a39bab3c3a695355a5853..e05839b7185567c158bf0ee0725159c598a4ca7c 100644 (file)
--- a/matitaB/components/content_pres/box.mli
+++ b/matitaB/components/content_pres/box.mli
@@ -63,7 +63,7 @@ val b_text: attr -> string -> 'expr box
 val b_object: 'expr -> 'expr box
 val b_indent: 'expr box -> 'expr box
 val b_space: 'expr box
-val b_kw: string -> 'expr box
+(* val b_kw: string -> 'expr box *)
 val b_toggle: 'expr box list -> 'expr box (** action which toggle among items *)
 
 val pp_attr: attr -> string

diff --git a/matitaB/components/content_pres/boxPp.ml b/matitaB/components/content_pres/boxPp.ml
index 7f71aa20bd81f8ffd0abbfb63a9c59a0cc19a851..9bf360a637d45fd1c5d654aae2e8007c19a832ce 100644 (file)
--- a/matitaB/components/content_pres/boxPp.ml
+++ b/matitaB/components/content_pres/boxPp.ml
@@ -40,8 +40,8 @@ let string_ink_len = utf8_string_length string_ink
 let contains_attrs contained container =
   List.for_all (fun attr -> List.mem attr container) contained
 
-let want_indent = contains_attrs (RenderingAttrs.indent_attributes `BoxML)
-let want_spacing = contains_attrs (RenderingAttrs.spacing_attributes `BoxML)
+let want_indent = contains_attrs (* (RenderingAttrs.indent_attributes `BoxML) *)[]
+let want_spacing = contains_attrs (* (RenderingAttrs.spacing_attributes `BoxML) *) []
 
 let shift off = List.map (fun (start,stop,v) -> start+off,stop+off,v);;
 
@@ -101,6 +101,7 @@ let fixed_rendering s =
   fun _ -> s_len,[s]
 
 let render_to_strings ~map_unicode_to_tex choose_action size markup =
+  prerr_endline ("render size is " ^ string_of_int size);
   let max_size = max_int in
   let rec aux_box =
     function
@@ -125,7 +126,7 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup =
             res
           else  (* break needed, re-render using a Box.V *)
             aux_box (Box.V (attrs, children)) size)
-    | Box.V (attrs, []) -> assert false
+    | Box.V (attrs, []) -> aux_box (Box.Text (attrs,"")) (* FIXME *)
     | Box.V (attrs, [child]) -> aux_box child
     | Box.V (attrs, hd :: tl) ->
         let indent = want_indent attrs in

diff --git a/matitaB/components/content_pres/cicNotationPres.ml b/matitaB/components/content_pres/cicNotationPres.ml
index 563af0b065454388fc7b88421c16f966ed148e22..30847816982ceb501d202ffb5152b846b7cb5a6e 100644 (file)
--- a/matitaB/components/content_pres/cicNotationPres.ml
+++ b/matitaB/components/content_pres/cicNotationPres.ml
@@ -161,8 +161,8 @@ let render status ?(prec=(-1)) =
     | A.Sup (A.Layout (A.Sub (t1,t2)), t3)
     | A.Sup (A.AttributedTerm (_,A.Layout (A.Sub (t1,t2))), t3)
       -> assert false
-    | A.Sub (t1, t2) -> assert false
-    | A.Sup (t1, t2) -> assert false
+    | A.Sub (t1, t2) -> Box.H ([],[aux prec t1;Box.Text ([],"_");aux prec t2])
+    | A.Sup (t1, t2) -> Box.H ([],[aux prec t1;Box.Text ([],"^");aux prec t2])
     | A.Below (t1, t2) -> assert false 
     | A.Above (t1, t2) -> assert false
     | A.Frac (t1, t2)
@@ -179,7 +179,7 @@ let render status ?(prec=(-1)) =
     | A.Maction alternatives -> 
          toggle_action (List.map invoke_reinit alternatives)
     | A.Group terms -> assert false 
-    | A.Break -> assert false 
+    | A.Break -> Box.Space [] 
   in
   aux prec
 

diff --git a/matitaB/components/content_pres/termContentPres.ml b/matitaB/components/content_pres/termContentPres.ml
index 27b55ebc1353e4594e0e5311f3aca72283e205f8..2b9bc650fcc9ec7b590e48e2ea27c25c5f0841d8 100644 (file)
--- a/matitaB/components/content_pres/termContentPres.ml
+++ b/matitaB/components/content_pres/termContentPres.ml
@@ -52,11 +52,11 @@ let rec remove_level_info =
   | Ast.AttributedTerm (a, t) -> Ast.AttributedTerm (a, remove_level_info t)
   | t -> t
 
-let add_xml_attrs attrs t =
-  if attrs = [] then t else Ast.AttributedTerm (`XmlAttrs attrs, t)
+let add_xml_attrs attrs t = t
+(*  if attrs = [] then t else Ast.AttributedTerm (`XmlAttrs attrs, t) *)
 
-let add_keyword_attrs =
-  add_xml_attrs (RenderingAttrs.keyword_attributes `MathML)
+let add_keyword_attrs t = t
+(*  add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) *)
 
 let box kind spacing indent content =
   Ast.Layout (Ast.Box ((kind, spacing, indent), content))
@@ -71,11 +71,11 @@ let builtin_symbol s = Ast.Literal (`Symbol s)
 let keyword k = add_keyword_attrs (Ast.Literal (`Keyword k))
 
 let number s =
-  add_xml_attrs (RenderingAttrs.number_attributes `MathML)
+  add_xml_attrs (* (RenderingAttrs.number_attributes `MathML) *) ()
     (Ast.Literal (`Number s))
 
 let ident i =
-  add_xml_attrs (RenderingAttrs.ident_attributes `MathML) 
+  add_xml_attrs (* (RenderingAttrs.ident_attributes `MathML) *) ()
     (Ast.Ident (i,`Ambiguous))
 
 let ident_w_href href i =
@@ -86,13 +86,13 @@ let ident_w_href href i =
       add_xml_attrs [Some "xlink", "href", href] (ident i)
 
 let binder_symbol s =
-  add_xml_attrs (RenderingAttrs.builtin_symbol_attributes `MathML)
+  add_xml_attrs (* (RenderingAttrs.builtin_symbol_attributes `MathML) *) ()
     (builtin_symbol s)
 
 let xml_of_sort x = 
   let to_string x = Ast.Ident (x, `Ambiguous) in
   let identify x = 
-    add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) (to_string x)
+    add_xml_attrs (* (RenderingAttrs.keyword_attributes `MathML) *) () (to_string x)
   in
   let lvl t = Ast.AttributedTerm (`Level 90,t) in
   match x with

diff --git a/matitaB/components/extlib/.depend b/matitaB/components/extlib/.depend
index f6168c1bc823d387308d6a448108d3e09ae7641f..6f707effcd8f40c3cca0262be1d045e17b98c5d2 100644 (file)
--- a/matitaB/components/extlib/.depend
+++ b/matitaB/components/extlib/.depend
@@ -19,8 +19,8 @@ hLog.cmo: hLog.cmi
 hLog.cmx: hLog.cmi 
 trie.cmo: trie.cmi 
 trie.cmx: trie.cmi 
-discrimination_tree.cmo: trie.cmi discrimination_tree.cmi 
-discrimination_tree.cmx: trie.cmx discrimination_tree.cmi 
+discrimination_tree.cmo: trie.cmi hExtlib.cmi discrimination_tree.cmi 
+discrimination_tree.cmx: trie.cmx hExtlib.cmx discrimination_tree.cmi 
 hTopoSort.cmo: hTopoSort.cmi 
 hTopoSort.cmx: hTopoSort.cmi 
 graphvizPp.cmo: graphvizPp.cmi 

diff --git a/matitaB/components/grafite_parser/.depend b/matitaB/components/grafite_parser/.depend
index b8b65a8c0e3da3caf2c210780184bc484807aca6..e5cd5f2b357785b3a6ea40ea0ec42b06723ecd31 100644 (file)
--- a/matitaB/components/grafite_parser/.depend
+++ b/matitaB/components/grafite_parser/.depend
@@ -1,8 +1,5 @@
-dependenciesParser.cmi: 
 grafiteParser.cmi: 
 print_grammar.cmi: grafiteParser.cmi 
-dependenciesParser.cmo: dependenciesParser.cmi 
-dependenciesParser.cmx: dependenciesParser.cmi 
 grafiteParser.cmo: grafiteParser.cmi 
 grafiteParser.cmx: grafiteParser.cmi 
 print_grammar.cmo: print_grammar.cmi 

diff --git a/matitaB/components/library/.depend b/matitaB/components/library/.depend
index 975c9e8da23e2873132c03c24be55dd65827dc92..edb2abe955afe4357fc9126c8296ddf87dd7247c 100644 (file)
--- a/matitaB/components/library/.depend
+++ b/matitaB/components/library/.depend
@@ -5,5 +5,5 @@ librarian.cmo: librarian.cmi
 librarian.cmx: librarian.cmi 
 libraryMisc.cmo: libraryMisc.cmi 
 libraryMisc.cmx: libraryMisc.cmi 
-libraryClean.cmo: libraryMisc.cmi libraryClean.cmi 
-libraryClean.cmx: libraryMisc.cmx libraryClean.cmi 
+libraryClean.cmo: libraryClean.cmi 
+libraryClean.cmx: libraryClean.cmi 

diff --git a/matitaB/components/ng_cic_content/interpretations.ml b/matitaB/components/ng_cic_content/interpretations.ml
index 598c93af706d5607c39e79477da5ced8288df410..c898c0faaf9c8e487cb429fabad72e46ec051395 100644 (file)
--- a/matitaB/components/ng_cic_content/interpretations.ml
+++ b/matitaB/components/ng_cic_content/interpretations.ml
@@ -483,7 +483,7 @@ let with_idrefs foo status obj =
 let nmap_obj status = with_idrefs nmap_obj0 status
 *)
 
-let nmap_obj = assert false
+let nmap_obj _ = assert false
 
 let nmap_sequent = nmap_sequent0 
 

diff --git a/matitaB/components/ng_cic_content/interpretations.mli b/matitaB/components/ng_cic_content/interpretations.mli
index b2c59b9c9b63e04ca2faa8af3dcb0e723525d250..4665be92c4a1d0e5f37cfe3bad36048e617dd28d 100644 (file)
--- a/matitaB/components/ng_cic_content/interpretations.mli
+++ b/matitaB/components/ng_cic_content/interpretations.mli
@@ -92,6 +92,4 @@ val nmap_sequent:
    NotationPt.sequent 
 
 val nmap_obj:
- #status -> NCic.obj ->
-  NotationPt.term Content.cobj *
-   (Content.id, NReference.reference) Hashtbl.t    (* id -> reference *)
+ #status -> NCic.obj -> NotationPt.term NotationPt.obj

diff --git a/matitaB/components/ng_disambiguation/.depend b/matitaB/components/ng_disambiguation/.depend
index e3e0e7d4412f307541f802f64b87a8b61a53d69b..0810bc8be9c2e8dce0593616b49c54eb617d961b 100644 (file)
--- a/matitaB/components/ng_disambiguation/.depend
+++ b/matitaB/components/ng_disambiguation/.depend
@@ -4,8 +4,8 @@ nCicDisambiguate.cmi:
 grafiteDisambiguate.cmi: 
 nnumber_notation.cmo: nnumber_notation.cmi 
 nnumber_notation.cmx: nnumber_notation.cmi 
-disambiguateChoices.cmo: disambiguateChoices.cmi 
-disambiguateChoices.cmx: disambiguateChoices.cmi 
+disambiguateChoices.cmo: nnumber_notation.cmi disambiguateChoices.cmi 
+disambiguateChoices.cmx: nnumber_notation.cmx disambiguateChoices.cmi 
 nCicDisambiguate.cmo: nCicDisambiguate.cmi 
 nCicDisambiguate.cmx: nCicDisambiguate.cmi 
 grafiteDisambiguate.cmo: nCicDisambiguate.cmi disambiguateChoices.cmi \

diff --git a/matitaB/components/ng_kernel/.depend b/matitaB/components/ng_kernel/.depend
index 7217cb5525bfa75c3330d8f744fbca7bb3b62963..0bf9955392720886e6a6a21314b78caeebd53421 100644 (file)
--- a/matitaB/components/ng_kernel/.depend
+++ b/matitaB/components/ng_kernel/.depend
@@ -4,9 +4,9 @@ nCicUtils.cmi: nCic.cmo
 nCicSubstitution.cmi: nCic.cmo 
 nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmo 
 nCicReduction.cmi: nCic.cmo 
-nCicPp.cmi: nReference.cmi nCic.cmo 
 nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmo 
 nCicUntrusted.cmi: nCic.cmo 
+nCicPp.cmi: nReference.cmi nCic.cmo 
 nCic.cmo: nUri.cmi nReference.cmi 
 nCic.cmx: nUri.cmx nReference.cmx 
 nUri.cmo: nUri.cmi 
@@ -22,13 +22,9 @@ nCicSubstitution.cmx: nReference.cmx nCicUtils.cmx nCic.cmx \
 nCicEnvironment.cmo: nUri.cmi nReference.cmi nCic.cmo nCicEnvironment.cmi 
 nCicEnvironment.cmx: nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi 
 nCicReduction.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
-    nCicPp.cmi nCicEnvironment.cmi nCic.cmo nCicReduction.cmi 
+    nCicEnvironment.cmi nCic.cmo nCicReduction.cmi 
 nCicReduction.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
-    nCicPp.cmx nCicEnvironment.cmx nCic.cmx nCicReduction.cmi 
-nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \
-    nCicEnvironment.cmi nCic.cmo nCicPp.cmi 
-nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \
-    nCicEnvironment.cmx nCic.cmx nCicPp.cmi 
+    nCicEnvironment.cmx nCic.cmx nCicReduction.cmi 
 nCicTypeChecker.cmo: nUri.cmi nReference.cmi nCicUtils.cmi \
     nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.cmi nCic.cmo \
     nCicTypeChecker.cmi 
@@ -39,3 +35,7 @@ nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
     nCicReduction.cmi nCicEnvironment.cmi nCic.cmo nCicUntrusted.cmi 
 nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
     nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi 
+nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \
+    nCicEnvironment.cmi nCic.cmo nCicPp.cmi 
+nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \
+    nCicEnvironment.cmx nCic.cmx nCicPp.cmi