From: Wilmer Ricciotti Date: Fri, 20 May 2011 09:59:31 +0000 (+0000) Subject: Compilation fix X-Git-Tag: make_still_working~2503 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6f020d79dea92003151e5e588fd73452f20ffb2c;p=helm.git Compilation fix --- diff --git a/matitaB/components/content/.depend b/matitaB/components/content/.depend index f4b4f3037..297edefdb 100644 --- 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 658d8d354..9d192c5b9 100644 --- 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 6e5bb4d92..74cc844e6 100644 --- 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 e7c2588eb..e05839b71 100644 --- 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 7f71aa20b..9bf360a63 100644 --- 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 563af0b06..308478169 100644 --- 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 27b55ebc1..2b9bc650f 100644 --- 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 f6168c1bc..6f707effc 100644 --- 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 b8b65a8c0..e5cd5f2b3 100644 --- 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 975c9e8da..edb2abe95 100644 --- 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 598c93af7..c898c0faa 100644 --- 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 b2c59b9c9..4665be92c 100644 --- 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 e3e0e7d44..0810bc8be 100644 --- 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 7217cb552..0bf995539 100644 --- 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