From: no author Date: Fri, 1 Dec 2000 20:00:19 +0000 (+0000) Subject: This commit was manufactured by cvs2svn to create tag 'V6-2'. X-Git-Tag: V6-2 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a59da263c7903b26597d5debcf2da1e0a4ccd686;p=helm.git This commit was manufactured by cvs2svn to create tag 'V6-2'. --- diff --git a/helm/dtd/annotations.dtd b/helm/dtd/annotations.dtd new file mode 100644 index 000000000..c7d379983 --- /dev/null +++ b/helm/dtd/annotations.dtd @@ -0,0 +1,29 @@ + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/cic.dtd b/helm/dtd/cic.dtd new file mode 100644 index 000000000..e16b10287 --- /dev/null +++ b/helm/dtd/cic.dtd @@ -0,0 +1,176 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/cicobject.dtd b/helm/dtd/cicobject.dtd new file mode 100644 index 000000000..1d9917b10 --- /dev/null +++ b/helm/dtd/cicobject.dtd @@ -0,0 +1,97 @@ + + + + + + + + + +%mathml; + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/cictypes.dtd b/helm/dtd/cictypes.dtd new file mode 100644 index 000000000..73d459263 --- /dev/null +++ b/helm/dtd/cictypes.dtd @@ -0,0 +1,16 @@ + + + + + + + + + +%cicdtd; + + + + + diff --git a/helm/dtd/isoamsa.ent b/helm/dtd/isoamsa.ent new file mode 100644 index 000000000..5ecf4db21 --- /dev/null +++ b/helm/dtd/isoamsa.ent @@ -0,0 +1,173 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isoamsb.ent b/helm/dtd/isoamsb.ent new file mode 100644 index 000000000..08e646c2b --- /dev/null +++ b/helm/dtd/isoamsb.ent @@ -0,0 +1,146 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isoamsc.ent b/helm/dtd/isoamsc.ent new file mode 100644 index 000000000..cce399cf9 --- /dev/null +++ b/helm/dtd/isoamsc.ent @@ -0,0 +1,49 @@ + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isoamsn.ent b/helm/dtd/isoamsn.ent new file mode 100644 index 000000000..cddeba066 --- /dev/null +++ b/helm/dtd/isoamsn.ent @@ -0,0 +1,117 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isoamso.ent b/helm/dtd/isoamso.ent new file mode 100644 index 000000000..8ac4bdb61 --- /dev/null +++ b/helm/dtd/isoamso.ent @@ -0,0 +1,77 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isoamsr.ent b/helm/dtd/isoamsr.ent new file mode 100644 index 000000000..7fec58255 --- /dev/null +++ b/helm/dtd/isoamsr.ent @@ -0,0 +1,205 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isobox.ent b/helm/dtd/isobox.ent new file mode 100644 index 000000000..630edc559 --- /dev/null +++ b/helm/dtd/isobox.ent @@ -0,0 +1,67 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isocyr1.ent b/helm/dtd/isocyr1.ent new file mode 100644 index 000000000..4bcc9e416 --- /dev/null +++ b/helm/dtd/isocyr1.ent @@ -0,0 +1,94 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isocyr2.ent b/helm/dtd/isocyr2.ent new file mode 100644 index 000000000..67c477b24 --- /dev/null +++ b/helm/dtd/isocyr2.ent @@ -0,0 +1,53 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isodia.ent b/helm/dtd/isodia.ent new file mode 100644 index 000000000..ba6496300 --- /dev/null +++ b/helm/dtd/isodia.ent @@ -0,0 +1,41 @@ + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isogrk3.ent b/helm/dtd/isogrk3.ent new file mode 100644 index 000000000..fa0335504 --- /dev/null +++ b/helm/dtd/isogrk3.ent @@ -0,0 +1,70 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isolat1.ent b/helm/dtd/isolat1.ent new file mode 100644 index 000000000..849d360ae --- /dev/null +++ b/helm/dtd/isolat1.ent @@ -0,0 +1,89 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isolat2.ent b/helm/dtd/isolat2.ent new file mode 100644 index 000000000..3049be7f1 --- /dev/null +++ b/helm/dtd/isolat2.ent @@ -0,0 +1,148 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isomfrk.ent b/helm/dtd/isomfrk.ent new file mode 100644 index 000000000..d3d92aaee --- /dev/null +++ b/helm/dtd/isomfrk.ent @@ -0,0 +1,79 @@ + + + +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > diff --git a/helm/dtd/isomopf.ent b/helm/dtd/isomopf.ent new file mode 100644 index 000000000..6b5e01f79 --- /dev/null +++ b/helm/dtd/isomopf.ent @@ -0,0 +1,53 @@ + + + +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > diff --git a/helm/dtd/isomscr.ent b/helm/dtd/isomscr.ent new file mode 100644 index 000000000..75d3bc5df --- /dev/null +++ b/helm/dtd/isomscr.ent @@ -0,0 +1,79 @@ + + + +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > diff --git a/helm/dtd/isonum.ent b/helm/dtd/isonum.ent new file mode 100644 index 000000000..d6d346169 --- /dev/null +++ b/helm/dtd/isonum.ent @@ -0,0 +1,106 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isopub.ent b/helm/dtd/isopub.ent new file mode 100644 index 000000000..5591fc390 --- /dev/null +++ b/helm/dtd/isopub.ent @@ -0,0 +1,111 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isotech.ent b/helm/dtd/isotech.ent new file mode 100644 index 000000000..8b30af833 --- /dev/null +++ b/helm/dtd/isotech.ent @@ -0,0 +1,183 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +" > + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/mathml2-qname-1.mod b/helm/dtd/mathml2-qname-1.mod new file mode 100644 index 000000000..4dea63a00 --- /dev/null +++ b/helm/dtd/mathml2-qname-1.mod @@ -0,0 +1,268 @@ + + + + + + + + + + + + + + + + + + + + + + + +]]> + + + + +]]> + + + + +]]> + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/mathml2.dtd b/helm/dtd/mathml2.dtd new file mode 100644 index 000000000..a9b7bf1ac --- /dev/null +++ b/helm/dtd/mathml2.dtd @@ -0,0 +1,1948 @@ + + + + + + + + + +%mathml-qname.mod;]]> + + +--> + +]]> + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +%ent-isoamsa; + + +%ent-isoamsb; + + +%ent-isoamsc; + + +%ent-isoamsn; + + +%ent-isoamso; + + +%ent-isoamsr; + + +%ent-isogrk3; + + +%ent-isomfrk; + + +%ent-isomopf; + + +%ent-isomscr; + + +%ent-isotech; + + + + +%ent-isobox; + + +%ent-isocyr1; + + +%ent-isocyr2; + + +%ent-isodia; + + +%ent-isolat1; + + +%ent-isolat2; + + +%ent-isonum; + + +%ent-isopub; + + + + +%ent-mmlextra; + + + + +%ent-mmlalias; + +]]> + + + + + + diff --git a/helm/dtd/maththeory.dtd b/helm/dtd/maththeory.dtd new file mode 100644 index 000000000..85469b6ce --- /dev/null +++ b/helm/dtd/maththeory.dtd @@ -0,0 +1,73 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/mmlalias.ent b/helm/dtd/mmlalias.ent new file mode 100644 index 000000000..f5901b384 --- /dev/null +++ b/helm/dtd/mmlalias.ent @@ -0,0 +1,529 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/mmlextra.ent b/helm/dtd/mmlextra.ent new file mode 100644 index 000000000..e76de448c --- /dev/null +++ b/helm/dtd/mmlextra.ent @@ -0,0 +1,134 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/provastruct.theory.xml b/helm/dtd/provastruct.theory.xml new file mode 100644 index 000000000..23c8f7c6d --- /dev/null +++ b/helm/dtd/provastruct.theory.xml @@ -0,0 +1,158 @@ + + + +
+ +
+ + cast + + Prop + + + Type + + + +
+ + cast + + Prop + + + Type + + + + 1: A 0: B + cast + + arrow + A + + arrow + arrow + A + + B + + + B + + + + + Prop + + + + 1: A 0: B + A0 + A + + H + arrow + A + + B + + + app + conj + A + B + A0 + app + axiom + A0 + H + + + + + + cast + + arrow + A + + arrow + arrow + A + + B + + + AB + + + + + Prop + + + +
+
+ + cast + + Set + + + Type + + + + 1: A + cast + + prodA + Prop + + arrow + A + + A + + + + + Prop + + + +
+ 0: A + A0 + Prop + + H + A0 + + H + + + + cast + + prodA + Prop + + arrow + A + + A + + + + + Prop + + + +
+
+ + diff --git a/helm/dtd/theoryobject.dtd b/helm/dtd/theoryobject.dtd new file mode 100644 index 000000000..8ff26cfb2 --- /dev/null +++ b/helm/dtd/theoryobject.dtd @@ -0,0 +1,14 @@ + + + + + + + + + +%cicobj; + + + + diff --git a/helm/interface/.cvsignore b/helm/interface/.cvsignore new file mode 100644 index 000000000..3a68425a2 --- /dev/null +++ b/helm/interface/.cvsignore @@ -0,0 +1,15 @@ +*.cmo +*.cmx +*.cmi + +experiment +experiment.opt +fix_params +fix_params.opt +mmlinterface +mmlinterface.opt +reduction +reduction.opt +t1lib.log +output.ps +output2.ps diff --git a/helm/interface/.depend b/helm/interface/.depend index a495dfeab..6402ae55b 100644 --- a/helm/interface/.depend +++ b/helm/interface/.depend @@ -82,6 +82,8 @@ deannotate.cmo: cic.cmo deannotate.cmx: cic.cmx cicXPath.cmo: cic.cmo cicXPath.cmx: cic.cmx +pxpUriResolver.cmo: configuration.cmo +pxpUriResolver.cmx: configuration.cmx annotationParser.cmo: annotationParser2.cmo pxpUriResolver.cmo annotationParser.cmx: annotationParser2.cmx pxpUriResolver.cmx annotationParser2.cmo: cic.cmo diff --git a/helm/interface/ISTRUZIONI b/helm/interface/ISTRUZIONI deleted file mode 100644 index fe6c09efc..000000000 --- a/helm/interface/ISTRUZIONI +++ /dev/null @@ -1,22 +0,0 @@ -============================== -ISTRUZIONI PER CHI USA LA TCSH -============================== - -Lanciare: - - source PER_FARLO_ANDARE_TCSH - -Poi far partire altri due xterm. -Nel primo lanciare: - - make start-xaland3 - -Nel secondo lanciare: - - make start-http-getter - -Se non funziona significa che ce ne e' gia' uno attivo. - -Infini lanciare, dall'ultima shell, - - ./mmlinterface.opt.saved diff --git a/helm/interface/Makefile b/helm/interface/Makefile index 2b892e2d9..d2fddf453 100644 --- a/helm/interface/Makefile +++ b/helm/interface/Makefile @@ -1,9 +1,10 @@ LABLGTK_DIR = /usr/lib/ocaml/lablgtk LABLGTK_MATHVIEW_DIR = /usr/lib/ocaml/lablgtk/mathview +MINIDOM_DIR = /usr/lib/ocaml/minidom PXP_DIR = /usr/lib/ocaml/site-lib/pxp NETSTRING_DIR = /usr/lib/ocaml/site-lib/netstring -OCAMLC = ocamlc -I $(LABLGTK_DIR) -I $(LABLGTK_MATHVIEW_DIR) -I $(PXP_DIR) -I $(NETSTRING_DIR) -I mlmathview -OCAMLOPT = ocamlopt -I $(LABLGTK_DIR) -I $(LABLGTK_MATHVIEW_DIR) -I mlgtk_devel -I $(PXP_DIR) -I $(NETSTRING_DIR) -I mlmathview +OCAMLC = ocamlc -I $(LABLGTK_DIR) -I $(LABLGTK_MATHVIEW_DIR) -I $(PXP_DIR) -I $(NETSTRING_DIR) -I $(MINIDOM_DIR) -I mlmathview +OCAMLOPT = ocamlopt -I $(LABLGTK_DIR) -I $(LABLGTK_MATHVIEW_DIR) -I mlgtk_devel -I $(PXP_DIR) -I $(NETSTRING_DIR) -I $(MINIDOM_DIR) -I mlmathview OCAMLDEP = ocamldep all: experiment reduction fix_params mmlinterface @@ -28,7 +29,7 @@ DEPOBJS = experiment.ml cicCache.ml cicCache.mli cicPp.ml cicPp.mli \ theoryParser.ml theoryParser2.ml theoryPp.ml theoryTypeChecker.ml \ cicCooking.ml cicCooking.mli cicFindParameters.ml theoryCache.ml \ fix_params.ml cic2Xml.ml xml.ml uriManager.ml uriManager.mli \ - cicSubstitution.ml cicSubstitution.mli mml.ml \ + cicSubstitution.ml cicSubstitution.mli \ mmlinterface.ml configuration.ml \ xsltProcessor.ml deannotate.ml cicXPath.ml pxpUriResolver.ml \ annotationParser.ml annotationParser2.ml annotation2Xml.ml \ @@ -39,7 +40,7 @@ MMLINTERFACEOBJS = configuration.cmo uriManager.cmo getter.cmo cic.cmo \ cicParser3.cmo cicParser2.cmo cicParser.cmo deannotate.cmo \ cicSubstitution.cmo annotationParser2.cmo \ annotationParser.cmo cicCache.cmo cicCooking.cmo cicPp.cmo \ - cicReduction.cmo cicTypeChecker.cmo mml.cmo \ + cicReduction.cmo cicTypeChecker.cmo \ xml.cmo \ xsltProcessor.cmo cic2Xml.cmo annotation2Xml.cmo \ cicXPath.cmo theory.cmo theoryParser2.cmo theoryParser.cmo \ @@ -52,7 +53,7 @@ MMLINTERFACEOPTOBJS = configuration.cmx uriManager.cmx getter.cmx cic.cmx \ deannotate.cmx cicSubstitution.cmx annotationParser2.cmx \ annotationParser.cmx cicCache.cmx \ cicCooking.cmx cicPp.cmx cicReduction.cmx \ - cicTypeChecker.cmx mml.cmx \ + cicTypeChecker.cmx \ xml.cmx xsltProcessor.cmx \ cic2Xml.cmx annotation2Xml.cmx cicXPath.cmx \ theory.cmx theoryParser2.cmx theoryParser.cmx \ @@ -105,23 +106,29 @@ depend: mmlinterface: $(MMLINTERFACEOBJS) $(OCAMLC) -custom -o mmlinterface str.cma unix.cma $(PXPLIBS) dbm.cma \ lablgtk.cma gtkInit.cmo \ + $(MINIDOM_DIR)/minidom.cmo \ + $(MINIDOM_DIR)/ominidom.cmo \ $(LABLGTK_MATHVIEW_DIR)/lablgtkmathview.cma \ $(MMLINTERFACEOBJS) \ -cclib "-lstr -L/usr/lib -L/usr/X11R6/lib -lgtk -lgdk \ -rdynamic -lgmodule -lglib -ldl -lXi -lXext -lX11 -lm \ - -lunix -L/usr/local/lib/gtkmathview -lgtkmathview \ - $(LABLGTK_MATHVIEW_DIR)/ml_gtk_mathview.o" \ + -lunix `gtkmathview-config --libs` \ + $(LABLGTK_MATHVIEW_DIR)/ml_gtk_mathview.o \ + $(MINIDOM_DIR)/ml_minidom.o" \ -cclib -lmldbm -cclib -lndbm mmlinterface.opt: $(MMLINTERFACEOPTOBJS) $(OCAMLOPT) -o mmlinterface.opt str.cmxa $(PXPLIBSOPT) unix.cmxa \ dbm.cmxa lablgtk.cmxa gtkInit.cmx \ + $(MINIDOM_DIR)/minidom.cmx \ + $(MINIDOM_DIR)/ominidom.cmx \ $(LABLGTK_MATHVIEW_DIR)/lablgtkmathview.cmxa \ $(MMLINTERFACEOPTOBJS) \ -cclib "-lstr -L/usr/lib -L/usr/X11R6/lib -lgtk -lgdk \ -rdynamic -lgmodule -lglib -ldl -lXi -lXext -lX11 -lm \ - -lunix -L/usr/local/lib/gtkmathview -lgtkmathview \ - $(LABLGTK_MATHVIEW_DIR)/ml_gtk_mathview.o" \ + -lunix `gtkmathview-config --libs` \ + $(LABLGTK_MATHVIEW_DIR)/ml_gtk_mathview.o \ + $(MINIDOM_DIR)/ml_minidom.o" \ -cclib -lmldbm -cclib -lndbm fix_params: $(FIX_PARAMSOBJS) @@ -164,17 +171,4 @@ clean: reduction.opt fix_params fix_params.opt mmlinterface \ mmlinterface.opt mmlinterface2 mmlinterface2.opt -start-xaland: - java xaland 12345 12346 examples/style/rootcontent.xsl \ - examples/style/annotatedpres.xsl examples/style/theory_content.xsl \ - examples/style/theory_pres.xsl - -start-xaland3: - java xaland 12347 12348 examples/style/rootcontent.xsl \ - examples/style/annotatedpres.xsl examples/style/theory_content.xsl \ - examples/style/theory_pres.xsl - -start-http-getter: - http_getter/http_getter.pl - include .depend diff --git a/helm/interface/NON_VA b/helm/interface/NON_VA deleted file mode 100644 index 375447103..000000000 --- a/helm/interface/NON_VA +++ /dev/null @@ -1,29 +0,0 @@ - - *********************************************************************** - - A T T E N Z I O N E ! ! ! - - Quando si usa fix_params.opt, scrivere - - find /really_very_local/helm/PARSER/examples - - invece di examples - - *********************************************************************** - - PROBLEMA NON FIXATO CON fix_params - - LA SOLUZIONE E' - - - -Correggere: - - examples/coq/SETS/Powerset_facts/Sets_as_an_algebra/setcover_intro.con.xml - -aggiungendo paramMode="POSSIBLE" - -Un esempio che altrimenti non funziona e': - -examples/coq/SETS/Powerset_Classical_facts/Sets_as_an_algebra/Add_covers.con.xml - diff --git a/helm/interface/PER_FARLO_ANDARE b/helm/interface/PER_FARLO_ANDARE deleted file mode 100644 index 20fb52a86..000000000 --- a/helm/interface/PER_FARLO_ANDARE +++ /dev/null @@ -1,2 +0,0 @@ -export LD_LIBRARY_PATH=.:/really_very_local/helm/proveluca/mml-browser/ -export no_proxy=cs.unibo.it diff --git a/helm/interface/PER_FARLO_ANDARE_TCSH b/helm/interface/PER_FARLO_ANDARE_TCSH deleted file mode 100644 index b527fabea..000000000 --- a/helm/interface/PER_FARLO_ANDARE_TCSH +++ /dev/null @@ -1,4 +0,0 @@ -setenv PATH "/home/projects/java/jdk1.2.2/bin:$PATH" -setenv CLASSPATH "/really_very_local/helm/java/xalan_1_1/xalan.jar:/really_very_local/helm/java/xalan_1_1/xerces.jar:." -setenv CLASSPATH "/really_very_local/helm/java/saxon-5.3.2/saxon.jar:$CLASSPATH" -setenv LD_LIBRARY_PATH ".:/really_very_local/helm/proveluca/mml-browser/" diff --git a/helm/interface/PER_FARLO_ANDARE_TCSH_D01 b/helm/interface/PER_FARLO_ANDARE_TCSH_D01 deleted file mode 100644 index 208f00a0e..000000000 --- a/helm/interface/PER_FARLO_ANDARE_TCSH_D01 +++ /dev/null @@ -1,4 +0,0 @@ -setenv PATH "/home/projects/java/jdk1.2.2/bin:$PATH" -setenv CLASSPATH "/really_very_local/helm/java/xalan_1_2_D01/xalan.jar:/really_very_local/helm/java/xalan_1_2_D01/xerces.jar:." -setenv CLASSPATH "/really_very_local/helm/java/saxon-5.3.2/saxon.jar:$CLASSPATH" -setenv LD_LIBRARY_PATH ".:/really_very_local/helm/proveluca/mml-browser/" diff --git a/helm/interface/cadet b/helm/interface/cadet index f674925b3..c9762da76 100755 --- a/helm/interface/cadet +++ b/helm/interface/cadet @@ -1,13 +1,19 @@ #! /bin/sh -export PATH=/home/cadet/sacerdot/jdk118/bin:$PATH +# Per (my)Coq 6.3.0 +export LD_LIBRARY_PATH=/usr/local/lib:$LD_LIBRARY_PATH -export CLASSPATH=/home/cadet/sacerdot/xalan-j_1_2/xalan.jar:/home/cadet/sacerdot/xalan-j_1_2/xerces.jar:. +# WARNING!!! No "//" in the middle of the path, nor a "/" at the end!!!! -#export CLASSPATH=$CLASSPATH:/home/lpadovan/helm/java/xalan_1_1/xalan.jar -#export CLASSPATH=$CLASSPATH:/home/lpadovan/helm/java/xalan_1_1/xerces.jar -#export CLASSPATH=$CLASSPATH:/home/lpadovan/helm/java/saxon-5.3.2/saxon.jar +#V6.2 +#export HELM_CONFIGURATION_PREFIX=~/HELM/installation -# Per (my)Coq 6.3.0 -#export LD_LIBRARY_PATH=/home/lpadovan/helm/usr/lib/:$LD_LIBRARY_PATH -export LD_LIBRARY_PATH=/usr/local/lib/gtkmathview:$LD_LIBRARY_PATH +#V7 +export HELM_CONFIGURATION_PREFIX=/home/cadet/sacerdot + +export T1LIB_CONFIG=./t1.config + +# Stix font +xset fp +xset fp+ ~/HELM/installation/fonts/ +xset fp rehash diff --git a/helm/interface/cicXPath.prima_degli_identificatori.ml b/helm/interface/cicXPath.prima_degli_identificatori.ml deleted file mode 100644 index 8a69d1a24..000000000 --- a/helm/interface/cicXPath.prima_degli_identificatori.ml +++ /dev/null @@ -1,102 +0,0 @@ -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 11/04/2000 *) -(* *) -(* *) -(******************************************************************************) - -(* functions to parse an XPath to retrieve the annotation *) - -exception WrongXPath of string;; - -let rec get_annotation_of_inductiveFun f xpath = - let module C = Cic in - match (xpath,f) with - 1::tl,(_,_,ty,_) -> get_annotation_of_term ty tl - | 2::tl,(_,_,_,te) -> get_annotation_of_term te tl - | l,_ -> - raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l "")) - -and get_annotation_of_coinductiveFun f xpath = - let module C = Cic in - match (xpath,f) with - 1::tl,(_,ty,_) -> get_annotation_of_term ty tl - | 2::tl,(_,_,te) -> get_annotation_of_term te tl - | l,_ -> - raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l "")) - -and get_annotation_of_inductiveType ty xpath = - let module C = Cic in - match (xpath,ty) with - 1::tl,(_,_,arity,_) -> get_annotation_of_term arity tl - | n::tl,(_,_,_,cons) when n <= List.length cons + 1 -> - let (_,ty,_) = List.nth cons (n-2) in - get_annotation_of_term ty tl - | l,_ -> - raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l "")) - -and get_annotation_of_term term xpath = - let module C = Cic in - match (xpath,term) with - [],C.ARel (_,ann,_,_) -> ann - | [],C.AVar (_,ann,_) -> ann - | [],C.AMeta (_,ann,_) -> ann - | [],C.ASort (_,ann,_) -> ann - | [],C.AImplicit (_,ann) -> ann - | [],C.ACast (_,ann,_,_) -> ann - | 1::tl,C.ACast (_,_,te,_) -> get_annotation_of_term te tl - | 2::tl,C.ACast (_,_,_,ty) -> get_annotation_of_term ty tl - | [],C.AProd (_,ann,_,_,_) -> ann - | 1::tl,C.AProd (_,_,_,so,_) -> get_annotation_of_term so tl - | 2::tl,C.AProd (_,_,_,_,ta) -> get_annotation_of_term ta tl - | [],C.ALambda (_,ann,_,_,_) -> ann - | 1::tl,C.ALambda (_,_,_,so,_) -> get_annotation_of_term so tl - | 2::tl,C.ALambda (_,_,_,_,ta) -> get_annotation_of_term ta tl - | [],C.AAppl (_,ann,_) -> ann - | n::tl,C.AAppl (_,_,l) when n <= List.length l -> - get_annotation_of_term (List.nth l (n-1)) tl - | [],C.AConst (_,ann,_,_) -> ann - | [],C.AAbst (_,ann,_) -> ann - | [],C.AMutInd (_,ann,_,_,_) -> ann - | [],C.AMutConstruct (_,ann,_,_,_,_) -> ann - | [],C.AMutCase (_,ann,_,_,_,_,_,_) -> ann - | 1::tl,C.AMutCase (_,_,_,_,_,outt,_,_) -> get_annotation_of_term outt tl - | 2::tl,C.AMutCase (_,_,_,_,_,_,te,_) -> get_annotation_of_term te tl - | n::tl,C.AMutCase (_,_,_,_,_,_,_,pl) when n <= List.length pl -> - get_annotation_of_term (List.nth pl (n-1)) tl - | [],C.AFix (_,ann,_,_) -> ann - | n::tl,C.AFix (_,_,_,fl) when n <= List.length fl -> - get_annotation_of_inductiveFun (List.nth fl (n-1)) tl - | [],C.ACoFix (_,ann,_,_) -> ann - | n::tl,C.ACoFix (_,_,_,fl) when n <= List.length fl -> - get_annotation_of_coinductiveFun (List.nth fl (n-1)) tl - | l,_ -> - raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l "")) -;; - -let get_annotation (annobj,_) xpath = - let module C = Cic in - match (xpath,annobj) with - [],C.ADefinition (_,ann,_,_,_,_) -> ann - | 1::tl,C.ADefinition (_,_,_,bo,_,_) -> get_annotation_of_term bo tl - | 2::tl,C.ADefinition (_,_,_,_,ty,_) -> get_annotation_of_term ty tl - | [],C.AAxiom (_,ann,_,_,_) -> ann - | 1::tl,C.AAxiom (_,_,_,ty,_) -> get_annotation_of_term ty tl - | [],C.AVariable (_,ann,_,_) -> ann - | 1::tl,C.AVariable (_,_,_,ty) -> get_annotation_of_term ty tl - | [],C.ACurrentProof (_,ann,_,_,_,_) -> ann - | n::tl,C.ACurrentProof (_,ann,_,conjs,_,_) when n <= List.length conjs -> - get_annotation_of_term (snd (List.nth conjs (n-1))) tl - | n::tl,C.ACurrentProof (_,ann,_,conjs,bo,_) when n = List.length conjs + 1 -> - get_annotation_of_term bo tl - | n::tl,C.ACurrentProof (_,ann,_,conjs,_,ty) when n = List.length conjs + 2 -> - get_annotation_of_term ty tl - | [],C.AInductiveDefinition (_,ann,_,_,_) -> ann - | n::tl,C.AInductiveDefinition (_,_,tys,_,_) when n <= List.length tys -> - get_annotation_of_inductiveType (List.nth tys (n-1)) tl - | l,_ -> - raise (WrongXPath (List.fold_right (fun n i -> string_of_int n ^ i) l "")) -;; diff --git a/helm/interface/configuration.ml b/helm/interface/configuration.ml index 6b0facf33..9a36cb37d 100644 --- a/helm/interface/configuration.ml +++ b/helm/interface/configuration.ml @@ -10,7 +10,14 @@ (******************************************************************************) (* this should be the only hard coded constant *) -let filename = "/home/cadet/sacerdot/local/etc/helm/configuration.xml";; +let filename = + let prefix = + try + Sys.getenv "HELM_CONFIGURATION_PREFIX" + with + Not_found -> "" + in + prefix ^ "/local/etc/helm/configuration.xml";; exception Warnings;; diff --git a/helm/interface/getter.ml b/helm/interface/getter.ml index 21c1901a1..d79409c89 100644 --- a/helm/interface/getter.ml +++ b/helm/interface/getter.ml @@ -56,6 +56,8 @@ let rec mk_urls_of_uris = uris map ;; +exception PerlGetterNotResponding;; + let update () = let module C = Configuration in let fd = open_in C.servers_file in @@ -72,7 +74,11 @@ let update () = Dbm.opendbm C.uris_dbm [Dbm.Dbm_wronly ; Dbm.Dbm_create] 0o660 in MapOfStrings.iter (fun uri url -> Dbm.add dbm uri url) urls_of_uris ; - Dbm.close dbm + Dbm.close dbm ; + (* Inform also the Perl-getter *) + if Sys.command ("wget -O /dev/null http://localhost:8081/update") <> 0 + then + raise PerlGetterNotResponding ; ;; (* url_of_uri : uri -> url *) @@ -115,8 +121,8 @@ let get uri = let module U = UriManager in get_file (U.uri_of_string - (Str.replace_first (Str.regexp "\.ann$") "" - (Str.replace_first (Str.regexp "\.types$") "" (U.string_of_uri uri)))) + (Str.replace_first (Str.regexp "\.types$") "" + (Str.replace_first (Str.regexp "\.ann$") "" (U.string_of_uri uri)))) ;; (* get_ann : uri -> filename *) diff --git a/helm/interface/gmon.out b/helm/interface/gmon.out deleted file mode 100644 index c48b8406f..000000000 Binary files a/helm/interface/gmon.out and /dev/null differ diff --git a/helm/interface/http_getter/http_getter.pl b/helm/interface/http_getter/http_getter.pl deleted file mode 100755 index 4ad358480..000000000 --- a/helm/interface/http_getter/http_getter.pl +++ /dev/null @@ -1,272 +0,0 @@ -#!/usr/bin/perl - -# next require defines: $helm_dir, $html_link -# LUCA - 12 sep 2000 -# require "/usr/lib/helm/configuration.pl"; -require "/home/cadet/sacerdot/local/lib/helm/configuration.pl"; -use HTTP::Daemon; -use HTTP::Status; -use HTTP::Request; -use LWP::UserAgent; -use DB_File; - -my $cont = ""; -my $d = new HTTP::Daemon LocalPort => 8081; -tie(%map, 'DB_File', 'urls_of_uris.db', O_RDONLY, 0664); -print "Please contact me at: url, ">\n"; -print "helm_dir: $helm_dir\n"; -$SIG{CHLD} = "IGNORE"; # do not accumulate defunct processes -while (my $c = $d->accept) { - if (fork() == 0) { - while (my $r = $c->get_request) { - #CSC: mancano i controlli di sicurezza - - $cont = ""; - my $cicuri = $r->url; - $cicuri =~ s/^[^?]*\?url=(.*)/$1/; - print "*".$r->url."\n"; - my $http_method = $r->method; - my $http_path = $r->url->path; - if ($http_method eq 'GET' and $http_path eq "/get") { - my $filename = $cicuri; - $filename =~ s/cic:(.*)/$1/; - $filename =~ s/theory:(.*)/$1/; - $filename = $helm_dir.$filename.".xml"; - my $resolved = $map{$cicuri}; - print "$cicuri ==> $resolved ($filename)\n"; - if (stat($filename)) { - print "Using local copy\n"; - open(FD, $filename); - while() { $cont .= $_; } - close(FD); - my $res = new HTTP::Response; - $res->content($cont); - $c->send_response($res); - } else { - print "Downloading\n"; - $ua = LWP::UserAgent->new; - $request = HTTP::Request->new(GET => "$resolved"); - $response = $ua->request($request, \&callback); - - print "Storing file\n"; - open(FD, $filename); - print FD $cont; - close(FD); - - my $res = new HTTP::Response; - $res->content($cont); - $c->send_response($res); - } - } elsif ($http_method eq 'GET' and $http_path eq "/annotate") { - my $do_annotate = ($cicuri =~ /\.ann$/); - my $target_to_annotate = $cicuri; - $target_to_annotate =~ s/(.*)\.ann$/$1/ if $do_annotate; - my $filename = $cicuri; - $filename =~ s/cic:(.*)/$1/; - $filename =~ s/theory:(.*)/$1/; - my $filename_target = $helm_dir.$filename if $do_annotate; - $filename = $helm_dir.$filename.".xml"; - $filename_target =~ s/(.*)\.ann$/$1.xml/ if $do_annotate; - my $resolved = $map{$cicuri}; - my $resolved_target = $map{$target_to_annotate} if $do_annotate; - if ($do_annotate) { - print "($cicuri, $target_to_annotate) ==> ($resolved + $resolved_target) ($filename)\n"; - } else { - print "$cicuri ==> $resolved ($filename)\n"; - } - - # Retrieves the annotation - - if (stat($filename)) { - print "Using local copy for the annotation\n"; - open(FD, $filename); - while() { $cont .= $_; } - close(FD); - } else { - print "Downloading the annotation\n"; - $ua = LWP::UserAgent->new; - $request = HTTP::Request->new(GET => "$resolved"); - $response = $ua->request($request, \&callback); - - print "Storing file for the annotation\n"; - open(FD, $filename); - print FD $cont; - close(FD); - } - my $annotation = $cont; - - # Retrieves the target to annotate - - $cont = ""; - if ($do_annotate) { - if (stat($filename_target)) { - print "Using local copy for the file to annotate\n"; - open(FD, $filename_target); - while() { $cont .= $_; } - close(FD); - } else { - print "Downloading the file to annotate\n"; - $ua = LWP::UserAgent->new; - $request = HTTP::Request->new(GET => "$resolved_target"); - $response = $ua->request($request, \&callback); - - print "Storing file for the file to annotate\n"; - open(FD, $filename_target); - print FD $cont; - close(FD); - } - } - my $target = $cont; - - # Merging the annotation and the target - - $target =~ s/<\?xml [^?]*\?>//sg; - $target =~ s/]*>//sg; - $annotation =~ s/<\?xml [^?]*\?>//sg; - $annotation =~ s/]*>//sg; - my $merged = < - -$target -$annotation - -EOT - - # Answering the client - - my $res = new HTTP::Response; - $res->content($merged); - $c->send_response($res); - } elsif ($http_method eq 'GET' and $http_path eq "/getwithtypes") { - my $do_annotate = ($cicuri =~ /\.types$/); - my $target_to_annotate = $cicuri; - $target_to_annotate =~ s/(.*)\.types$/$1/ if $do_annotate; - my $filename = $cicuri; - $filename =~ s/cic:(.*)/$1/; - $filename =~ s/theory:(.*)/$1/; - my $filename_target = $helm_dir.$filename if $do_annotate; - $filename = $helm_dir.$filename.".xml"; - $filename_target =~ s/(.*)\.types$/$1.xml/ if $do_annotate; - my $resolved = $map{$cicuri}; - my $resolved_target = $map{$target_to_annotate} if $do_annotate; - if ($do_annotate) { - print "GETWITHTYPES!!\n"; - print "($cicuri, $target_to_annotate) ==> ($resolved + $resolved_target) ($filename)\n"; - } else { - print "$cicuri ==> $resolved ($filename)\n"; - } - - # Retrieves the annotation - - if (stat($filename)) { - print "Using local copy for the types\n"; - open(FD, $filename); - while() { $cont .= $_; } - close(FD); - } else { - print "Downloading the types\n"; - $ua = LWP::UserAgent->new; - $request = HTTP::Request->new(GET => "$resolved"); - $response = $ua->request($request, \&callback); - - print "Storing file for the types\n"; - open(FD, $filename); - print FD $cont; - close(FD); - } - my $annotation = $cont; - - # Retrieves the target to annotate - - $cont = ""; - my $target; - if ($do_annotate) { - if (stat($filename_target)) { - print "Using local copy for the file to type\n"; - open(FD, $filename_target); - while() { $cont .= $_; } - close(FD); - } else { - print "Downloading the file to type\n"; - $ua = LWP::UserAgent->new; - $request = HTTP::Request->new(GET => "$resolved_target"); - $response = $ua->request($request, \&callback); - - print "Storing file for the file to type\n"; - open(FD, $filename_target); - print FD $cont; - close(FD); - } - $target = $cont; - } else { - $target = $annotation; - $annotation = ""; - } - - # Merging the annotation and the target - - $target =~ s/<\?xml [^?]*\?>//sg; - $target =~ s/]*>//sg; - $annotation =~ s/<\?xml [^?]*\?>//sg; - $annotation =~ s/]*>//sg; - my $merged = < - -$target - -$annotation - - -EOT - - # Answering the client - - my $res = new HTTP::Response; - $res->content($merged); - $c->send_response($res); - } elsif ($http_method eq 'GET' and $http_path eq "/getdtd") { - my $filename = $cicuri; - $filename = $helm_dir."/dtd/".$filename; - print "DTD: $cicuri ==> ($filename)\n"; - if (stat($filename)) { - print "Using local copy\n"; - open(FD, $filename); - while() { $cont .= $_; } - close(FD); - my $res = new HTTP::Response; - $res->content($cont); - $c->send_response($res); - } else { - die "Could not find DTD!"; - } - } elsif ($http_method eq 'GET' and $http_path eq "/conf") { - my $quoted_html_link = $html_link; - $quoted_html_link =~ s/&/&/g; - $quoted_html_link =~ s//>/g; - $quoted_html_link =~ s/'/'/g; - $quoted_html_link =~ s/"/"/g; - print "Configuration requested, returned #$quoted_html_link#\n"; - $cont = "$quoted_html_link"; - my $res = new HTTP::Response; - $res->content($cont); - $c->send_response($res); - } else { - print "INVALID REQUEST!!!!!\n"; - $c->send_error(RC_FORBIDDEN) - } - } - $c->close; - undef($c); - print "\nCONNECTION CLOSED\n\n"; - exit; - } # fork -} - -#================================ - -sub callback -{ - my ($data) = @_; - $cont .= $data; -} diff --git a/helm/interface/http_getter/http_getter.pl2 b/helm/interface/http_getter/http_getter.pl2 deleted file mode 100755 index 3adfa2be0..000000000 --- a/helm/interface/http_getter/http_getter.pl2 +++ /dev/null @@ -1,199 +0,0 @@ -#!/usr/bin/perl - -# next require defines: $helm_dir, $html_link -require "/usr/lib/helm/configuration.pl"; -use HTTP::Daemon; -use HTTP::Status; -use HTTP::Request; -use LWP::UserAgent; -use DB_File; - -my $cont = ""; -my $d = new HTTP::Daemon LocalPort => 8081; -tie(%map, 'DB_File', 'urls_of_uris.db', O_RDONLY, 0664); -print "Please contact me at: url, ">\n"; -print "helm_dir: $helm_dir\n"; -$SIG{CHLD} = "IGNORE"; # do not accumulate defunct processes -while (my $c = $d->accept) { - if (fork() == 0) { - while (my $r = $c->get_request) { - #CSC: mancano i controlli di sicurezza - - $cont = ""; - my $cicuri = $r->url; - $cicuri =~ s/^[^?]*\?url=(.*)/$1/; - print "*".$r->url."\n"; - my $http_method = $r->method; - my $http_path = $r->url->path; - if ($http_method eq 'GET' and $http_path eq "/get") { - my $filename = $cicuri; - $filename =~ s/cic:(.*)/$1/; - $filename =~ s/theory:(.*)/$1/; - $filename = $helm_dir.$filename.".xml"; - my $resolved = $map{$cicuri}; - print "$cicuri ==> $resolved ($filename)\n"; - if (stat($filename)) { - print "Using local copy\n"; - open(FD, $filename); - while() { $cont .= $_; } - close(FD); - my $res = new HTTP::Response; - $res->content($cont); - $c->send_response($res); - } else { - print "Downloading\n"; - $ua = LWP::UserAgent->new; - $request = HTTP::Request->new(GET => "$resolved"); - $response = $ua->request($request, \&callback); - - print "Storing file\n"; - open(FD, $filename); - print FD $cont; - close(FD); - - my $res = new HTTP::Response; - $res->content($cont); - $c->send_response($res); - } - } elsif ($http_method eq 'GET' and $http_path eq "/annotate") { - my $do_annotate = ($cicuri =~ /\.ann$/); - my $target_to_annotate = $cicuri; - $target_to_annotate =~ s/(.*)\.ann$/$1/ if $do_annotate; - my $filename = $cicuri; - $filename =~ s/cic:(.*)/$1/; - $filename =~ s/theory:(.*)/$1/; - my $filename_target = $helm_dir.$filename if $do_annotate; - $filename = $helm_dir.$filename.".xml"; - $filename_target =~ s/(.*)\.ann$/$1.xml/ if $do_annotate; - my $resolved = $map{$cicuri}; - my $resolved_target = $map{$target_to_annotate} if $do_annotate; - if ($do_annotate) { - print "($cicuri, $target_to_annotate) ==> ($resolved + $resolved_target) ($filename)\n"; - } elsif ($http_method eq 'GET' and $http_path eq "/getwithtypes") { - my $do_annotate = ($cicuri =~ /\.types$/); - my $target_to_annotate = $cicuri; - $target_to_annotate =~ s/(.*)\.types$/$1/ if $do_annotate; - my $filename = $cicuri; - $filename =~ s/cic:(.*)/$1/; - $filename =~ s/theory:(.*)/$1/; - my $filename_target = $helm_dir.$filename if $do_annotate; - $filename = $helm_dir.$filename.".xml"; - $filename_target =~ s/(.*)\.types$/$1.xml/ if $do_annotate; - my $resolved = $map{$cicuri}; - my $resolved_target = $map{$target_to_annotate} if $do_annotate; - if ($do_annotate) { - print "($cicuri, $target_to_annotate) ==> ($resolved + $resolved_target) ($filename)\n"; - } else { - print "$cicuri ==> $resolved ($filename)\n"; - } - - # Retrieves the annotation - - if (stat($filename)) { - print "Using local copy for the types\n"; - open(FD, $filename); - while() { $cont .= $_; } - close(FD); - } else { - print "Downloading the types\n"; - $ua = LWP::UserAgent->new; - $request = HTTP::Request->new(GET => "$resolved"); - $response = $ua->request($request, \&callback); - - print "Storing file for the types\n"; - open(FD, $filename); - print FD $cont; - close(FD); - } - my $annotation = $cont; - - # Retrieves the target to annotate - - $cont = ""; - if ($do_annotate) { - if (stat($filename_target)) { - print "Using local copy for the file to type\n"; - open(FD, $filename_target); - while() { $cont .= $_; } - close(FD); - } else { - print "Downloading the file to type\n"; - $ua = LWP::UserAgent->new; - $request = HTTP::Request->new(GET => "$resolved_target"); - $response = $ua->request($request, \&callback); - - print "Storing file for the file to type\n"; - open(FD, $filename_target); - print FD $cont; - close(FD); - } - } - my $target = $cont; - - # Merging the annotation and the target - - $target =~ s/<\?xml [^?]*\?>//sg; - $target =~ s/]*>//sg; - $annotation =~ s/<\?xml [^?]*\?>//sg; - $annotation =~ s/]*>//sg; - my $merged = < - -$target - -$annotation - - -EOT - - # Answering the client - - my $res = new HTTP::Response; - $res->content($merged); - $c->send_response($res); - } elsif ($http_method eq 'GET' and $http_path eq "/getdtd") { - my $filename = $cicuri; - $filename = $helm_dir."/dtd/".$filename; - print "DTD: $cicuri ==> ($filename)\n"; - if (stat($filename)) { - print "Using local copy\n"; - open(FD, $filename); - while() { $cont .= $_; } - close(FD); - my $res = new HTTP::Response; - $res->content($cont); - $c->send_response($res); - } else { - die "Could not find DTD!"; - } - } elsif ($http_method eq 'GET' and $http_path eq "/conf") { - my $quoted_html_link = $html_link; - $quoted_html_link =~ s/&/&/g; - $quoted_html_link =~ s//>/g; - $quoted_html_link =~ s/'/'/g; - $quoted_html_link =~ s/"/"/g; - print "Configuration requested, returned #$quoted_html_link#\n"; - $cont = "$quoted_html_link"; - my $res = new HTTP::Response; - $res->content($cont); - $c->send_response($res); - } else { - print "INVALID REQUEST!!!!!\n"; - $c->send_error(RC_FORBIDDEN) - } - } - $c->close; - undef($c); - print "\nCONNECTION CLOSED\n\n"; - exit; - } # fork -} - -#================================ - -sub callback -{ - my ($data) = @_; - $cont .= $data; -} diff --git a/helm/interface/isterix b/helm/interface/isterix index a1f696a3b..a7d6c4d3e 100755 --- a/helm/interface/isterix +++ b/helm/interface/isterix @@ -1,12 +1,16 @@ #! /bin/sh -export PATH=$PATH:/opt/java/jdk118/bin/ +# WARNING!!! No "//" in the middle of the path, nor a "/" at the end!!!! -export CLASSPATH=. -export CLASSPATH=$CLASSPATH:/home/lpadovan/helm/java/xalan_1_1/xalan.jar -export CLASSPATH=$CLASSPATH:/home/lpadovan/helm/java/xalan_1_1/xerces.jar -export CLASSPATH=$CLASSPATH:/home/lpadovan/helm/java/saxon-5.3.2/saxon.jar +#V6.2 # Per (my)Coq 6.3.0 export LD_LIBRARY_PATH=/home/lpadovan/helm/usr/lib/:$LD_LIBRARY_PATH -export LD_LIBRARY_PATH=/usr/local/lib/gtkmathview:$LD_LIBRARY_PATH +export LD_LIBRARY_PATH=/usr/local/lib/:$LD_LIBRARY_PATH + +#export T1LIB_CONFIG=./t1.config + +# Stix font +#xset fp +#xset fp+ ~/HELM/installation/fonts/ +#xset fp rehash diff --git a/helm/interface/javacore15005.txt b/helm/interface/javacore15005.txt deleted file mode 100644 index 992096462..000000000 --- a/helm/interface/javacore15005.txt +++ /dev/null @@ -1,195 +0,0 @@ -SIGSEGV received at bfffeacc in /home/cadet/sacerdot/jdk118/lib/linux/native_threads/libjitc.so. Processing terminated -java full version "JDK 1.1.8 IBM build l118-19991013 (JIT enabled: jitc)" -args: /home/cadet/sacerdot/jdk118/bin/linux/native_threads/java xaland 12345 12346 examples/style/annotatedcont.xsl examples/style/annotatedpres.xsl examples/style/theory_content.xsl examples/style/theory_pres.xsl - -Operating Environment ---------------------- -Host : cadet. -OS Level : 2.2.14-5.0smp.#1 SMP Tue Mar 7 21:01:40 EST 2000 -glibc Version : 2.1.3 -No. of Procs : 1 -Memory Info: - total: used: free: shared: buffers: cached: -Mem: 64503808 55078912 9424896 36126720 1527808 18075648 -Swap: 133885952 7442432 126443520 -MemTotal: 62992 kB -MemFree: 9204 kB -MemShared: 35280 kB -Buffers: 1492 kB -Cached: 17652 kB -BigTotal: 0 kB -BigFree: 0 kB -SwapTotal: 130748 kB -SwapFree: 123480 kB - -Application Environment ------------------------ -Signal Handlers - - SIGQUIT : ignored - SIGILL : sysThreadIDump (libjava.so) - SIGABRT : sysThreadIDump (libjava.so) - SIGFPE : sysThreadIDump (libjava.so) - SIGBUS : sysThreadIDump (libjava.so) - SIGSEGV : sysThreadIDump (libjava.so) - SIGPIPE : ignored - SIGUSR1 : doSuspendLoop (libjava.so) - -Environment Variables - - LESSOPEN=|/usr/bin/lesspipe.sh %s - SAL_DO_NOT_USE_INVERT50=true - HISTSIZE=1000 - HOSTNAME=cadet - LOGNAME=sacerdot - VISUAL=/usr/bin/emacs - LD_LIBRARY_PATH=/home/cadet/sacerdot/jdk118/lib/linux/native_threads:/usr/local/lib/gtkmathview:/home/pauillac/coq3/sacerdot/rvplayer5.0 - MAIL=/var/spool/mail/sacerdot - PAGER=less - CLASSPATH=.:/usr/share/java/bsf.jar:/usr/share/java/xalan.jar:/usr/share/java/xerces.jar:/home/cadet/sacerdot/jdk118/classes:/home/cadet/sacerdot/jdk118/lib/classes.jar:/home/cadet/sacerdot/jdk118/lib/rt.jar:/home/cadet/sacerdot/jdk118/lib/i18n.jar:/home/cadet/sacerdot/jdk118/lib/classes.zip - LESSCHARDEF=8bcccbcc18b95.33b. - ARCH=i586 - PROMPT=cad: - TERM=xterm - HOSTTYPE=i386 - PATH=/home/cadet/sacerdot/jdk118/bin:/home/pauillac/coq3/sacerdot/bin/i586:/home/pauillac/coq3/sacerdot/bin:/usr/bin/X11:/usr/bin:/usr/local/bin:/usr/ucb:/usr/bin:/bin:/usr/sbin:/sbin:/usr/games:. - PRINTER=hp11rv - HOME=/home/pauillac/coq3/sacerdot - SHELL=/bin/sh - ELANLIB=/home/pauillac/coq3/sacerdot/elan-dist.3.00/elanlib - PILOTPORT=/dev/ttyS1 - TEXINPUTS=:.:/home/pauillac/coq3/sacerdot/lib/latex/inputs:/usr/local/lib/tex/inputs3 - USER=sacerdot - ENSCRIPT=-Php11rvl -2 -r -B -L66 -k -h - MANPATH=/usr/man/preformat:/usr/man:/usr/X11/man:/usr/local/man:/home/pauillac/coq3/sacerdot/man - LESS=-m -e -q -d - JAVA_HOME=/home/cadet/sacerdot/jdk118 - DISPLAY=:0.0 - MAKEFLAGS= - HOST=cadet - OSTYPE=Linux - NNTPSERVER=news-rocq.inria.fr - WINDOWID=54525966 - SHLVL=4 - MAKELEVEL=1 - LS_COLORS=no=00:fi=00:di=01;34:ln=01;36:pi=40;33:so=01;35:bd=40;33;01:cd=40;33;01:or=01;05;37;41:mi=01;05;37;41:ex=01;32:*.cmd=01;32:*.exe=01;32:*.com=01;32:*.btm=01;32:*.bat=01;32:*.sh=01;32:*.csh=01;32:*.tar=01;31:*.tgz=01;31:*.arj=01;31:*.taz=01;31:*.lzh=01;31:*.zip=01;31:*.z=01;31:*.Z=01;31:*.gz=01;31:*.bz2=01;31:*.bz=01;31:*.tz=01;31:*.rpm=01;31:*.cpio=01;31:*.jpg=01;35:*.gif=01;35:*.bmp=01;35:*.xbm=01;35:*.xpm=01;35:*.png=01;35:*.tif=01;35: - EDITOR=/usr/bin/emacs - MFLAGS= - CVSROOT=/net/pauillac/constr/ARCHIVE - - -Current Thread Details ----------------------- - "main" (TID:0x402e62d8, sys_thread_t:0x804abe0) - Native Thread State: ThreadID: 00000400 Reuse: 1 USER PRIMORDIAL RUNNING - Native Stack Data : base: bffff47c pointer bffbf96c used(260880) free(-13072) - ----- Monitors held ----- - ----- Native stack ----- - - - - - - - - - ?? - ?? - ?? - - java_lang_Compiler_start - - __irem_trap6 - ------ Java stack ------ () prio=5 *current thread* - org.apache.xalan.xslt.XSLTEngineImpl.createStylesheetRoot(XSLTEngineImpl.java:715) - org.apache.xalan.xslt.XSLTEngineImpl.processStylesheet(Compiled Code) - org.apache.xalan.xslt.XSLTEngineImpl.processStylesheet(Compiled Code) - xaland.main(Compiled Code) ----------------------------------------------------------------------- - - -Total Thread Count: 3 -Active Thread Count: 3 -JNI Thread Count: 0 - -Full thread dump: - "Async Garbage Collector" (TID:0x402e6238, sys_thread_t:0x8091f50) - Native Thread State: ThreadID: 00000803 Reuse: 1 DAEMON MONITOR WAIT - Native Stack Data : base: bf5ffd84 pointer bf5ffb78 used(524) free(247284) - ----- Monitors held ----- - ----- Native stack ----- - sysMonitorWait - sysThreadSleep - threadSleep - SetOrigArgs - sysThread_shell - pthread_detach - __clone - ------ Java stack ------ () prio=1 ----------------------------------------------------------------------- - - "Finalizer thread" (TID:0x402e6288, sys_thread_t:0x8091cd0) - Native Thread State: ThreadID: 00000402 Reuse: 1 DAEMON MONITOR WAIT - Native Stack Data : base: bf7ffd84 pointer bf7ffbec used(408) free(247400) - ----- Monitors held ----- - ----- Native stack ----- - sysMonitorWait - waiting on Finalize me queue lock - finalizeOnExit - sysThread_shell - pthread_detach - __clone - ------ Java stack ------ () prio=1 ----------------------------------------------------------------------- - - "main" (TID:0x402e62d8, sys_thread_t:0x804abe0) - Native Thread State: ThreadID: 00000400 Reuse: 1 USER PRIMORDIAL RUNNING - Native Stack Data : base: bffff47c pointer bffbf960 used(260892) free(-13084) - ----- Monitors held ----- - ----- Native stack ----- - - - - - - - - - ?? - ?? - ?? - - java_lang_Compiler_start - - __irem_trap6 - ------ Java stack ------ () prio=5 *current thread* - org.apache.xalan.xslt.XSLTEngineImpl.createStylesheetRoot(XSLTEngineImpl.java:715) - org.apache.xalan.xslt.XSLTEngineImpl.processStylesheet(Compiled Code) - org.apache.xalan.xslt.XSLTEngineImpl.processStylesheet(Compiled Code) - xaland.main(Compiled Code) ----------------------------------------------------------------------- - - -System Monitor Status ---------------------- - JIT monitor: unowned. - JIT monitor: unowned. - JIT monitor: unowned. - JIT monitor: unowned. - JIT monitor: unowned. - Thread queue lock: unowned. - Name and type hash table lock: unowned. - String intern lock: unowned. - JNI pinning lock: unowned. - JNI global reference lock: unowned. - Zip lock: unowned. - BinClass lock: unowned. - Class loading lock: unowned. - Java stack lock: unowned. - Code rewrite lock: unowned. - Heap Lock: unowned. - Has finalization queue lock: unowned. - Finalize me queue lock: unowned. - Integer lock access-lock: unowned. - Monitor cache lock: unowned. - Monitor registry: unowned. - -Object Monitor Status ---------------------- diff --git a/helm/interface/javacore15021.txt b/helm/interface/javacore15021.txt deleted file mode 100644 index bac0b8a76..000000000 --- a/helm/interface/javacore15021.txt +++ /dev/null @@ -1,195 +0,0 @@ -SIGSEGV received at bfffeacc in /home/cadet/sacerdot/jdk118/lib/linux/native_threads/libjitc.so. Processing terminated -java full version "JDK 1.1.8 IBM build l118-19991013 (JIT enabled: jitc)" -args: /home/cadet/sacerdot/jdk118/bin/linux/native_threads/java xaland 12345 12346 examples/style/annotatedcont.xsl examples/style/annotatedpres.xsl examples/style/theory_content.xsl examples/style/theory_pres.xsl - -Operating Environment ---------------------- -Host : cadet. -OS Level : 2.2.14-5.0smp.#1 SMP Tue Mar 7 21:01:40 EST 2000 -glibc Version : 2.1.3 -No. of Procs : 1 -Memory Info: - total: used: free: shared: buffers: cached: -Mem: 64503808 55672832 8830976 36130816 1536000 18612224 -Swap: 133885952 7442432 126443520 -MemTotal: 62992 kB -MemFree: 8624 kB -MemShared: 35284 kB -Buffers: 1500 kB -Cached: 18176 kB -BigTotal: 0 kB -BigFree: 0 kB -SwapTotal: 130748 kB -SwapFree: 123480 kB - -Application Environment ------------------------ -Signal Handlers - - SIGQUIT : ignored - SIGILL : sysThreadIDump (libjava.so) - SIGABRT : sysThreadIDump (libjava.so) - SIGFPE : sysThreadIDump (libjava.so) - SIGBUS : sysThreadIDump (libjava.so) - SIGSEGV : sysThreadIDump (libjava.so) - SIGPIPE : ignored - SIGUSR1 : doSuspendLoop (libjava.so) - -Environment Variables - - LESSOPEN=|/usr/bin/lesspipe.sh %s - SAL_DO_NOT_USE_INVERT50=true - HISTSIZE=1000 - HOSTNAME=cadet - LOGNAME=sacerdot - VISUAL=/usr/bin/emacs - LD_LIBRARY_PATH=/home/cadet/sacerdot/jdk118/lib/linux/native_threads:/usr/local/lib/gtkmathview:/home/pauillac/coq3/sacerdot/rvplayer5.0 - MAIL=/var/spool/mail/sacerdot - PAGER=less - CLASSPATH=.:/usr/share/java/bsf.jar:/usr/share/java/xalan.jar:/usr/share/java/xerces.jar:/home/cadet/sacerdot/jdk118/classes:/home/cadet/sacerdot/jdk118/lib/classes.jar:/home/cadet/sacerdot/jdk118/lib/rt.jar:/home/cadet/sacerdot/jdk118/lib/i18n.jar:/home/cadet/sacerdot/jdk118/lib/classes.zip - LESSCHARDEF=8bcccbcc18b95.33b. - ARCH=i586 - PROMPT=cad: - TERM=xterm - HOSTTYPE=i386 - PATH=/home/cadet/sacerdot/jdk118/bin:/home/pauillac/coq3/sacerdot/bin/i586:/home/pauillac/coq3/sacerdot/bin:/usr/bin/X11:/usr/bin:/usr/local/bin:/usr/ucb:/usr/bin:/bin:/usr/sbin:/sbin:/usr/games:. - PRINTER=hp11rv - HOME=/home/pauillac/coq3/sacerdot - SHELL=/bin/sh - ELANLIB=/home/pauillac/coq3/sacerdot/elan-dist.3.00/elanlib - PILOTPORT=/dev/ttyS1 - TEXINPUTS=:.:/home/pauillac/coq3/sacerdot/lib/latex/inputs:/usr/local/lib/tex/inputs3 - USER=sacerdot - ENSCRIPT=-Php11rvl -2 -r -B -L66 -k -h - MANPATH=/usr/man/preformat:/usr/man:/usr/X11/man:/usr/local/man:/home/pauillac/coq3/sacerdot/man - LESS=-m -e -q -d - JAVA_HOME=/home/cadet/sacerdot/jdk118 - DISPLAY=:0.0 - MAKEFLAGS= - HOST=cadet - OSTYPE=Linux - NNTPSERVER=news-rocq.inria.fr - WINDOWID=54525966 - SHLVL=4 - MAKELEVEL=1 - LS_COLORS=no=00:fi=00:di=01;34:ln=01;36:pi=40;33:so=01;35:bd=40;33;01:cd=40;33;01:or=01;05;37;41:mi=01;05;37;41:ex=01;32:*.cmd=01;32:*.exe=01;32:*.com=01;32:*.btm=01;32:*.bat=01;32:*.sh=01;32:*.csh=01;32:*.tar=01;31:*.tgz=01;31:*.arj=01;31:*.taz=01;31:*.lzh=01;31:*.zip=01;31:*.z=01;31:*.Z=01;31:*.gz=01;31:*.bz2=01;31:*.bz=01;31:*.tz=01;31:*.rpm=01;31:*.cpio=01;31:*.jpg=01;35:*.gif=01;35:*.bmp=01;35:*.xbm=01;35:*.xpm=01;35:*.png=01;35:*.tif=01;35: - EDITOR=/usr/bin/emacs - MFLAGS= - CVSROOT=/net/pauillac/constr/ARCHIVE - - -Current Thread Details ----------------------- - "main" (TID:0x402e62d8, sys_thread_t:0x804abe0) - Native Thread State: ThreadID: 00000400 Reuse: 1 USER PRIMORDIAL RUNNING - Native Stack Data : base: bffff47c pointer bffbf96c used(260880) free(-13072) - ----- Monitors held ----- - ----- Native stack ----- - - - - - - - - - ?? - ?? - ?? - - java_lang_Compiler_start - - __irem_trap6 - ------ Java stack ------ () prio=5 *current thread* - org.apache.xalan.xslt.XSLTEngineImpl.createStylesheetRoot(XSLTEngineImpl.java:715) - org.apache.xalan.xslt.XSLTEngineImpl.processStylesheet(Compiled Code) - org.apache.xalan.xslt.XSLTEngineImpl.processStylesheet(Compiled Code) - xaland.main(Compiled Code) ----------------------------------------------------------------------- - - -Total Thread Count: 3 -Active Thread Count: 3 -JNI Thread Count: 0 - -Full thread dump: - "Async Garbage Collector" (TID:0x402e6238, sys_thread_t:0x8091f50) - Native Thread State: ThreadID: 00000803 Reuse: 1 DAEMON MONITOR WAIT - Native Stack Data : base: bf5ffd84 pointer bf5ffb78 used(524) free(247284) - ----- Monitors held ----- - ----- Native stack ----- - sysMonitorWait - sysThreadSleep - threadSleep - SetOrigArgs - sysThread_shell - pthread_detach - __clone - ------ Java stack ------ () prio=1 ----------------------------------------------------------------------- - - "Finalizer thread" (TID:0x402e6288, sys_thread_t:0x8091cd0) - Native Thread State: ThreadID: 00000402 Reuse: 1 DAEMON MONITOR WAIT - Native Stack Data : base: bf7ffd84 pointer bf7ffbec used(408) free(247400) - ----- Monitors held ----- - ----- Native stack ----- - sysMonitorWait - waiting on Finalize me queue lock - finalizeOnExit - sysThread_shell - pthread_detach - __clone - ------ Java stack ------ () prio=1 ----------------------------------------------------------------------- - - "main" (TID:0x402e62d8, sys_thread_t:0x804abe0) - Native Thread State: ThreadID: 00000400 Reuse: 1 USER PRIMORDIAL RUNNING - Native Stack Data : base: bffff47c pointer bffbf960 used(260892) free(-13084) - ----- Monitors held ----- - ----- Native stack ----- - - - - - - - - - ?? - ?? - ?? - - java_lang_Compiler_start - - __irem_trap6 - ------ Java stack ------ () prio=5 *current thread* - org.apache.xalan.xslt.XSLTEngineImpl.createStylesheetRoot(XSLTEngineImpl.java:715) - org.apache.xalan.xslt.XSLTEngineImpl.processStylesheet(Compiled Code) - org.apache.xalan.xslt.XSLTEngineImpl.processStylesheet(Compiled Code) - xaland.main(Compiled Code) ----------------------------------------------------------------------- - - -System Monitor Status ---------------------- - JIT monitor: unowned. - JIT monitor: unowned. - JIT monitor: unowned. - JIT monitor: unowned. - JIT monitor: unowned. - Thread queue lock: unowned. - Name and type hash table lock: unowned. - String intern lock: unowned. - JNI pinning lock: unowned. - JNI global reference lock: unowned. - Zip lock: unowned. - BinClass lock: unowned. - Class loading lock: unowned. - Java stack lock: unowned. - Code rewrite lock: unowned. - Heap Lock: unowned. - Has finalization queue lock: unowned. - Finalize me queue lock: unowned. - Integer lock access-lock: unowned. - Monitor cache lock: unowned. - Monitor registry: unowned. - -Object Monitor Status ---------------------- diff --git a/helm/interface/latinize.pl b/helm/interface/latinize.pl deleted file mode 100755 index 7fa678736..000000000 --- a/helm/interface/latinize.pl +++ /dev/null @@ -1,10 +0,0 @@ -#!/usr/bin/perl - -while() -{ - s/→/->/g; - s/⇒/=>/g; - s/λ/\\/g; - s/Π/||/g; - print; -} diff --git a/helm/interface/mkindex.sh b/helm/interface/mkindex.sh deleted file mode 100755 index b47864fae..000000000 --- a/helm/interface/mkindex.sh +++ /dev/null @@ -1,3 +0,0 @@ -#!/bin/bash - -echo `find . -name "*.xml"` | /really_very_local/helm/PARSER/coq_like_pretty_printer/uris_of_filenames.pl > index.txt diff --git a/helm/interface/mml.dtd b/helm/interface/mml.dtd deleted file mode 100644 index 10ce5cb5d..000000000 --- a/helm/interface/mml.dtd +++ /dev/null @@ -1,55 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/interface/mml.ml b/helm/interface/mml.ml deleted file mode 100644 index 88c281350..000000000 --- a/helm/interface/mml.ml +++ /dev/null @@ -1,11 +0,0 @@ -type expr = - Null - | Mi of string - | Mo of string - | Mn of string - | Mtext of string - | Mrow of expr list - | Mfenced of string * string * string * expr list (* open, close, separators *) -type fragment = - Math of expr list -;; diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml index 76f6e5a78..5cd0faf0c 100755 --- a/helm/interface/mmlinterface.ml +++ b/helm/interface/mmlinterface.ml @@ -109,7 +109,6 @@ let to_visit_uris = ref [];; exception NoCurrentUri;; exception NoNextOrPrevUri;; -exception GtkInterfaceInternalError;; let theory_get_current_uri () = match !theory_visited_uris with @@ -205,19 +204,32 @@ let prev rendering_window () = ;; (* called when an hyperlink is clicked *) -let jump rendering_window s = - let uri = UriManager.uri_of_string s in - rendering_window#show () ; - rendering_window#prevb#misc#set_sensitive true ; - rendering_window#nextb#misc#set_sensitive false ; - visited_uris := uri::!visited_uris ; - to_visit_uris := [] ; - annotated_obj := None ; - update_output rendering_window uri +let jump rendering_window (node : Ominidom.o_mDOMNode) = + let module O = Ominidom in + match (node#get_attribute (O.o_mDOMString_of_string "href")) with + Some str -> + let s = str#get_string in + let uri = UriManager.uri_of_string s in + rendering_window#show () ; + rendering_window#prevb#misc#set_sensitive true ; + rendering_window#nextb#misc#set_sensitive false ; + visited_uris := uri::!visited_uris ; + to_visit_uris := [] ; + annotated_obj := None ; + update_output rendering_window uri + | None -> assert false ;; -let changefont rendering_window () = - rendering_window#output#set_font_size rendering_window#spinb#value_as_int +let choose_selection rendering_window (node : Ominidom.o_mDOMNode option) = + let module O = Ominidom in + let rec aux node = + match node#get_attribute (O.o_mDOMString_of_string "xref") with + Some _ -> rendering_window#output#set_selection (Some node) + | None -> aux (node#get_parent) + in + match node with + Some x -> aux x + | None -> rendering_window#output#set_selection None ;; @@ -313,16 +325,17 @@ let check rendering_window () = ;; let annotateb_pressed rendering_window annotation_window () = - let xpath = (rendering_window#output#get_selection : string option) in - match xpath with - None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n" + let module O = Ominidom in + match rendering_window#output#get_selection with + | Some node -> + begin + match (node#get_attribute (O.o_mDOMString_of_string "xref")) with | Some xpath -> - try let annobj = get_annotated_obj () (* next "cast" can't got rid of, but I don't know why *) and annotation = (annotation_window#annotation : GEdit.text) in - ann := CicXPath.get_annotation annobj xpath ; - CicAnnotationHinter.create_hints annotation_window annobj xpath ; + ann := CicXPath.get_annotation annobj (xpath#get_string) ; + CicAnnotationHinter.create_hints annotation_window annobj (xpath#get_string) ; annotation#delete_text 0 annotation#length ; begin match !(!ann) with @@ -338,11 +351,12 @@ let annotateb_pressed rendering_window annotation_window () = end ; GMain.Grab.add (annotation_window#window_to_annotate#coerce) ; annotation_window#show () ; - with - e -> + | None -> (* next "cast" can't got rid of, but I don't know why *) let errors = (rendering_window#errors : GEdit.text) in - errors#insert ("\n" ^ Printexc.to_string e ^ "\n") + errors#insert ("\nNo xref found\n") + end + | None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n" ;; (* called when the annotation is confirmed *) @@ -352,7 +366,7 @@ let save_annotation annotation = else !ann := None ; match !annotated_obj with - None -> raise GtkInterfaceInternalError + None -> assert false | Some (annobj,_) -> let uri = get_current_uri () in let annxml = Annotation2Xml.pp_annotation annobj uri in @@ -385,12 +399,121 @@ let mktree selection_changed rendering_window = ignore(treeitem2#connect#select (selection_changed rendering_window uri)) ; aux treeitem2 ti - ) !content + ) (List.sort compare !content) | _ -> () in aux ;; +(* Stuff for the widget settings *) + +let export_to_postscript (output : GMathView.math_view) () = + output#export_to_postscript ~filename:"output.ps" (); +;; + +let activate_t1 output button_set_anti_aliasing button_set_kerning + button_export_to_postscript button_t1 () += + let is_set = button_t1#active in + output#set_font_manager_type + (if is_set then `font_manager_t1 else `font_manager_gtk) ; + if is_set then + begin + button_set_anti_aliasing#misc#set_sensitive true ; + button_set_kerning#misc#set_sensitive true ; + button_export_to_postscript#misc#set_sensitive true ; + end + else + begin + button_set_anti_aliasing#misc#set_sensitive false ; + button_set_kerning#misc#set_sensitive false ; + button_export_to_postscript#misc#set_sensitive false ; + end +;; + +let set_anti_aliasing output button_set_anti_aliasing () = + output#set_anti_aliasing button_set_anti_aliasing#active +;; + +let set_kerning output button_set_kerning () = + output#set_kerning button_set_kerning#active +;; + +let changefont output font_size_spinb () = + output#set_font_size font_size_spinb#value_as_int +;; + +let set_log_verbosity output log_verbosity_spinb () = + output#set_log_verbosity log_verbosity_spinb#value_as_int +;; + +class settings_window output sw button_export_to_postscript jump_callback + selection_changed_callback += + let settings_window = GWindow.window ~title:"GtkMathView settings" () in + let vbox = + GPack.vbox ~packing:settings_window#add () in + let table = + GPack.table + ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5 + ~border_width:5 ~packing:vbox#add () in + let button_t1 = + GButton.toggle_button ~label:"activate t1 fonts" + ~packing:(table#attach ~left:0 ~top:0) () in + let button_set_anti_aliasing = + GButton.toggle_button ~label:"set_anti_aliasing" + ~packing:(table#attach ~left:1 ~top:0) () in + let button_set_kerning = + GButton.toggle_button ~label:"set_kerning" + ~packing:(table#attach ~left:2 ~top:0) () in + let table = + GPack.table + ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5 + ~border_width:5 ~packing:vbox#add () in + let font_size_label = + GMisc.label ~text:"font size:" + ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in + let font_size_spinb = + let sadj = + GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 () + in + GEdit.spin_button + ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in + let log_verbosity_label = + GMisc.label ~text:"log verbosity:" + ~packing:(table#attach ~left:0 ~top:1) () in + let log_verbosity_spinb = + let sadj = + GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 () + in + GEdit.spin_button + ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let closeb = + GButton.button ~label:"Close" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in +object(self) + method show = settings_window#show + initializer + button_set_anti_aliasing#misc#set_sensitive false ; + button_set_kerning#misc#set_sensitive false ; + (* Signals connection *) + ignore(button_t1#connect#clicked + (activate_t1 output button_set_anti_aliasing button_set_kerning + button_export_to_postscript button_t1)) ; + ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ; + ignore(button_set_anti_aliasing#connect#toggled + (set_anti_aliasing output button_set_anti_aliasing)); + ignore(button_set_kerning#connect#toggled + (set_kerning output button_set_kerning)) ; + ignore(log_verbosity_spinb#connect#changed + (set_log_verbosity output log_verbosity_spinb)) ; + ignore(closeb#connect#clicked settings_window#misc#hide) +end;; + +(* Main windows *) + class annotation_window output label = let window_to_annotate = GWindow.window ~title:"Annotating environment" ~border_width:2 () in @@ -450,7 +573,8 @@ object (self) in visited_uris := new_current_uri::(List.tl !visited_uris) ; label#set_text (UriManager.string_of_uri new_current_uri) ; - output#load (parse_no_cache new_current_uri) + let mmlfile = parse_no_cache new_current_uri in + output#load mmlfile )) ; ignore (abortb#connect#clicked (fun () -> @@ -473,7 +597,7 @@ class rendering_window annotation_window output (label : GMisc.label) = GPack.vbox ~packing:window#add () in let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in let paned = - GPack.paned `HORIZONTAL ~packing:(vbox#pack ~padding:5) () in + GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in let scrolled_window0 = GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in let _ = scrolled_window0#add output#coerce in @@ -495,13 +619,12 @@ class rendering_window annotation_window output (label : GMisc.label) = let annotateb = GButton.button ~label:"Annotate" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let spinb = - let sadj = - GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 () - in - GEdit.spin_button - ~adjustment:sadj ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) - () in + let settingsb = + GButton.button ~label:"Settings" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let button_export_to_postscript = + GButton.button ~label:"export_to_postscript" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let closeb = GButton.button ~label:"Close" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in @@ -509,22 +632,26 @@ object(self) method nextb = nextb method prevb = prevb method label = label - method spinb = spinb method output = (output : GMathView.math_view) method errors = errors method show () = window#show () initializer nextb#misc#set_sensitive false ; prevb#misc#set_sensitive false ; + button_export_to_postscript#misc#set_sensitive false ; (* signal handlers here *) ignore(output#connect#jump (jump self)) ; + ignore(output#connect#selection_changed (choose_selection self)) ; ignore(nextb#connect#clicked (next self)) ; ignore(prevb#connect#clicked (prev self)) ; ignore(checkb#connect#clicked (check self)) ; - ignore(spinb#connect#changed (changefont self)) ; ignore(closeb#connect#clicked window#misc#hide) ; ignore(annotateb#connect#clicked (annotateb_pressed self annotation_window)) ; + let settings_window = new settings_window output scrolled_window0 + button_export_to_postscript (jump self) (choose_selection self) in + ignore(settingsb#connect#clicked settings_window#show) ; + ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ; ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) end;; @@ -537,7 +664,7 @@ class theory_rendering_window rendering_window = GMisc.label ~text:"???" ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let paned = - GPack.paned `HORIZONTAL ~packing:(vbox#pack ~padding:5) () in + GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in let scrolled_window0 = GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in let output = @@ -557,13 +684,12 @@ class theory_rendering_window rendering_window = let checkb = GButton.button ~label:"Check" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let spinb = - let sadj = - GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 () - in - GEdit.spin_button - ~adjustment:sadj ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) - () in + let settingsb = + GButton.button ~label:"Settings" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let button_export_to_postscript = + GButton.button ~label:"export_to_postscript" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let closeb = GButton.button ~label:"Close" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in @@ -573,18 +699,22 @@ object(self) method label = label method output = (output : GMathView.math_view) method errors = errors - method spinb = spinb method show () = window#show () initializer nextb#misc#set_sensitive false ; prevb#misc#set_sensitive false ; + button_export_to_postscript#misc#set_sensitive false ; (* signal handlers here *) ignore(output#connect#jump (jump rendering_window)) ; + ignore(output#connect#selection_changed (choose_selection self)) ; ignore(nextb#connect#clicked (theory_next self)) ; ignore(prevb#connect#clicked (theory_prev self)) ; ignore(checkb#connect#clicked (theory_check self)) ; - ignore(spinb#connect#changed (changefont self)) ; + let settings_window = new settings_window output scrolled_window0 + button_export_to_postscript (jump rendering_window)(choose_selection self) in + ignore(settingsb#connect#clicked settings_window#show) ; + ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ; ignore(closeb#connect#clicked window#misc#hide) ; ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) end;; diff --git a/helm/interface/mmlinterface.opt.saved b/helm/interface/mmlinterface.opt.saved deleted file mode 100755 index cb5708ade..000000000 Binary files a/helm/interface/mmlinterface.opt.saved and /dev/null differ diff --git a/helm/interface/pxpUriResolver.ml b/helm/interface/pxpUriResolver.ml index b5b37f398..ad8713cf3 100644 --- a/helm/interface/pxpUriResolver.ml +++ b/helm/interface/pxpUriResolver.ml @@ -10,12 +10,12 @@ let resolve = function - "http://localhost:8081/getdtd?url=cic.dtd" -> - "/home/pauillac/coq3/sacerdot/HELM/INTERFACE/examples/dtd/cic.dtd" - | "http://localhost:8081/getdtd?url=maththeory.dtd" -> - "/home/pauillac/coq3/sacerdot/HELM/INTERFACE/examples/dtd/maththeory.dtd" - | "http://localhost:8081/getdtd?url=annotations.dtd" -> - "/home/pauillac/coq3/sacerdot/HELM/INTERFACE/examples/dtd/annotations.dtd" + "http://localhost:8081/getdtd?uri=cic.dtd" -> + Configuration.dtd_dir ^ "/cic.dtd" + | "http://localhost:8081/getdtd?uri=maththeory.dtd" -> + Configuration.dtd_dir ^ "/maththeory.dtd" + | "http://localhost:8081/getdtd?uri=annotations.dtd" -> + Configuration.dtd_dir ^ "/annotations.dtd" | s -> s ;; diff --git a/helm/interface/servers.txt b/helm/interface/servers.txt deleted file mode 100644 index b91a71522..000000000 --- a/helm/interface/servers.txt +++ /dev/null @@ -1,2 +0,0 @@ -http://caristudenti.students.cs.unibo.it/~sacerdot/helm -http://pagadebit.students.cs.unibo.it/really_very_local/helm/PARSER/examples diff --git a/helm/interface/servers.txt.universita b/helm/interface/servers.txt.universita deleted file mode 100755 index c24a58cad..000000000 --- a/helm/interface/servers.txt.universita +++ /dev/null @@ -1,2 +0,0 @@ -http://phd.cs.unibo.it/helm/PARSER/examples -http://caristudenti.students.cs.unibo.it/~sacerdot/helm diff --git a/helm/interface/t1.config b/helm/interface/t1.config new file mode 100644 index 000000000..afb669e95 --- /dev/null +++ b/helm/interface/t1.config @@ -0,0 +1,3 @@ +ENCODING=. +AFM=/usr/share/texmf/fonts/afm/ +TYPE1=/usr/share/texmf/fonts/type1/bluesky/cm/:/usr/X11R6/lib/X11/fonts/Type1/:. diff --git a/helm/interface/uris_of_filenames.pl b/helm/interface/uris_of_filenames.pl index d738f51b7..e06ac822a 100755 --- a/helm/interface/uris_of_filenames.pl +++ b/helm/interface/uris_of_filenames.pl @@ -4,7 +4,7 @@ while() { chomp; split / /; for (@_) { - if (/.*\.(con|var|ind)\.xml/) + if (/.*\.(con|var|ind)(\.types)?\.xml/) { s/\./cic:/; } elsif (/.*\.theory\.xml/) { s/\./theory:/; } diff --git a/helm/interface/urls_of_uris.db b/helm/interface/urls_of_uris.db deleted file mode 100644 index ef6b46a51..000000000 Binary files a/helm/interface/urls_of_uris.db and /dev/null differ diff --git a/helm/interface/xaland-cpp/xaland.cpp b/helm/interface/xaland-cpp/xaland.cpp deleted file mode 100644 index e22140267..000000000 --- a/helm/interface/xaland-cpp/xaland.cpp +++ /dev/null @@ -1,207 +0,0 @@ -// Base header file. Must be first. -#include - -#include -#include - -#include - -#include - -#include - -#include -#include -#include - -#include -#include -#include -#include -#include -#include -#include - -#include -#include - -int main(int argc, const char* []) -{ -#if !defined(XALAN_NO_NAMESPACES) - using std::cerr; - using std::endl; - using std::ofstream; -#endif - - if (argc != 1) { - cerr << "Usage: SimpleTransform" - << endl - << endl; - } else { - try { - // Call the static initializer for Xerces... - XMLPlatformUtils::Initialize(); - - { - // Initialize the Xalan XSLT subsystem... - XSLTInit theInit; - - // Create the support objects that are necessary for - // running the processor... - XercesDOMSupport theDOMSupport; - XercesParserLiaison theParserLiaison(theDOMSupport); - XPathSupportDefault theXPathSupport(theDOMSupport); - XSLTProcessorEnvSupportDefault theXSLTProcessorEnvSupport; - XObjectFactoryDefault theXObjectFactory; - XPathFactoryDefault theXPathFactory; - - // Create a processor... - XSLTEngineImpl theProcessor( - theParserLiaison, - theXPathSupport, - theXSLTProcessorEnvSupport, - theDOMSupport, - theXObjectFactory, - theXPathFactory); - - // Connect the processor to the support object... - theXSLTProcessorEnvSupport.setProcessor(&theProcessor); - - // Create a stylesheet construction context, and a stylesheet - // execution context... - StylesheetConstructionContextDefault theConstructionContext( - theProcessor, - theXSLTProcessorEnvSupport, - theXPathFactory); - - StylesheetExecutionContextDefault theExecutionContext( - theProcessor, - theXSLTProcessorEnvSupport, - theXPathSupport, - theXObjectFactory); - - // Our input files...The assumption is that the executable will be - // run from same directory as the input files. - const XalanDOMString theXMLFileName("foo.xml"); - const XalanDOMString theXSLFileName("foo.xsl"); - - // Our input sources... - XSLTInputSource theInputSource(c_wstr(theXMLFileName)); - XSLTInputSource theStylesheetSource(c_wstr(theXSLFileName)); - - // Our output target... - const XalanDOMString theOutputFileName("foo.out"); - XSLTResultTarget theResultTarget(theOutputFileName); - - theProcessor.process( - theInputSource, - theStylesheetSource, - theResultTarget, - theConstructionContext, - theExecutionContext); - - } - - // Call the static terminator for Xerces... - XMLPlatformUtils::Terminate(); - } - catch(...) { - cerr << "Exception caught!!!" - << endl - << endl; - } - } - - return 0; -} - -/**************************************************/ -/* - -public class xaland { - public static void Transform(StylesheetRoot style, String xmlSourceURL, String OutputURL) throws java.io.IOException, java.net.MalformedURLException, org.xml.sax.SAXException - { - XSLTInputSource xmlSource = new XSLTInputSource (xmlSourceURL); - XSLTResultTarget xmlResult = new XSLTResultTarget (OutputURL); - style.process(xmlSource, xmlResult); - } - - public static void main(String argv[]) throws java.io.IOException, java.net.MalformedURLException, org.xml.sax.SAXException - { - int port = Integer.parseInt(argv[0]); - int port2 = Integer.parseInt(argv[1]); - String xsl1 = argv[2]; - String xsl2 = argv[3]; - String theory_xsl1 = argv[4]; - String theory_xsl2 = argv[5]; - - XSLTProcessor theory_processor = - XSLTProcessorFactory.getProcessor(new org.apache.xalan.xpath.xdom.XercesLiaison()); - StylesheetRoot theory_style1 = - theory_processor.processStylesheet(theory_xsl1); - theory_processor.reset(); - StylesheetRoot theory_style2 = - theory_processor.processStylesheet(theory_xsl2); - theory_processor.setStylesheet(theory_style2); - - XSLTProcessor processor = - XSLTProcessorFactory.getProcessor(new org.apache.xalan.xpath.xdom.XercesLiaison()); - StylesheetRoot style1 = processor.processStylesheet(xsl1); - processor.reset(); - StylesheetRoot style2 = processor.processStylesheet(xsl2); - processor.setStylesheet(style2); - - DatagramSocket socket = new DatagramSocket(port); - - System.out.println("Demon activated on input port " + port + - " and output port " + port2); - while(true) { - System.out.print("Ready..."); - - /* Warning: the packet must be a fresh one! * / - DatagramPacket packet = new DatagramPacket(new byte[1024],1024); - socket.receive(packet); - byte data[] = packet.getData(); - int datalen = packet.getLength(); - String received = new String(data,0,datalen); - - int first = received.indexOf(' '); - int last = received.lastIndexOf(' '); - String mode = received.substring(0,first); - String input = received.substring(first+1,last); - String output = received.substring(last+1); - - System.out.println("request received! Parameters are"); - System.out.println("Mode: " + mode + " "); - System.out.println("Input file: \"" + input + "\""); - System.out.println("Output file: \"" + output + "\"\n"); - - if ((new File(output)).exists()) { - System.out.println("Using cached version\n"); - } else { - FileOutputStream fout = new FileOutputStream(output); - if (mode.equals("cic")) { - processor.setDocumentHandler(style2.getSAXSerializer(fout)); - XSLTResultTarget content = new XSLTResultTarget(processor); - style1.process(new XSLTInputSource(input), content); - } else if (mode.equals("theory")) { - theory_processor.setDocumentHandler( - theory_style2.getSAXSerializer(fout)); - XSLTResultTarget content = - new XSLTResultTarget(theory_processor); - theory_style1.process(new XSLTInputSource(input), content); - } - } - - InetAddress address = InetAddress.getLocalHost(); - DatagramSocket socket2 = new DatagramSocket(); - - byte buf[] = new byte[0]; - DatagramPacket packet2 = new DatagramPacket(buf,0,address,port2); - - socket2.send(packet2); - } - } -} - -*/ diff --git a/helm/interface/xaland-java/rompi.class b/helm/interface/xaland-java/rompi.class deleted file mode 100644 index 4abfe3865..000000000 Binary files a/helm/interface/xaland-java/rompi.class and /dev/null differ diff --git a/helm/interface/xaland-java/rompi.java b/helm/interface/xaland-java/rompi.java deleted file mode 100644 index 6a633dbc9..000000000 --- a/helm/interface/xaland-java/rompi.java +++ /dev/null @@ -1,12 +0,0 @@ -import java.net.*; - -public class rompi { - public static void main(String argv[]) throws java.io.IOException, java.net.MalformedURLException - { - /* Wait forever ;-) */ - DatagramSocket socket2 = new DatagramSocket(12346); - DatagramPacket packet2 = new DatagramPacket(new byte[1],1); - System.out.println("Ho preso il socket e non lo lascio piu', caro pu, caro pu"); - socket2.receive(packet2); - } -} diff --git a/helm/interface/xaland-java/sped.class b/helm/interface/xaland-java/sped.class deleted file mode 100644 index cc6f53dac..000000000 Binary files a/helm/interface/xaland-java/sped.class and /dev/null differ diff --git a/helm/interface/xaland-java/sped.java b/helm/interface/xaland-java/sped.java deleted file mode 100644 index 9d96610d4..000000000 --- a/helm/interface/xaland-java/sped.java +++ /dev/null @@ -1,28 +0,0 @@ -import java.net.*; - -public class sped { - public static void main(String argv[]) throws java.io.IOException, java.net.MalformedURLException - { - String input = argv[0]; - String out1 = argv[1]; - String out2 = argv[2]; - - String sent = input + " " + out1 + " " + out2; - - InetAddress address = InetAddress.getLocalHost(); - DatagramSocket socket = new DatagramSocket(); - - int strlen = sent.length(); - byte buf[] = new byte[strlen]; - sent.getBytes(0,strlen,buf,0); - DatagramPacket packet = new DatagramPacket(buf,strlen,address,12345); - - socket.send(packet); - - - /* Wait for answer (or forever ;-) */ - DatagramSocket socket2 = new DatagramSocket(12346); - DatagramPacket packet2 = new DatagramPacket(new byte[1],1); - socket2.receive(packet2); - } -} diff --git a/helm/interface/xaland-java/xaland.class b/helm/interface/xaland-java/xaland.class deleted file mode 100644 index 6871fda4b..000000000 Binary files a/helm/interface/xaland-java/xaland.class and /dev/null differ diff --git a/helm/interface/xaland-java/xaland.java b/helm/interface/xaland-java/xaland.java deleted file mode 100644 index 9eda83124..000000000 --- a/helm/interface/xaland-java/xaland.java +++ /dev/null @@ -1,89 +0,0 @@ -import org.apache.xalan.xslt.*; -import java.net.*; -import java.io.*; - -public class xaland { - public static void Transform(StylesheetRoot style, String xmlSourceURL, String OutputURL) throws java.io.IOException, java.net.MalformedURLException, org.xml.sax.SAXException - { - XSLTInputSource xmlSource = new XSLTInputSource (xmlSourceURL); - XSLTResultTarget xmlResult = new XSLTResultTarget (OutputURL); - style.process(xmlSource, xmlResult); - } - - public static void main(String argv[]) throws java.io.IOException, java.net.MalformedURLException, org.xml.sax.SAXException - { - int port = Integer.parseInt(argv[0]); - int port2 = Integer.parseInt(argv[1]); - String xsl1 = argv[2]; - String xsl2 = argv[3]; - String theory_xsl1 = argv[4]; - String theory_xsl2 = argv[5]; - - XSLTProcessor theory_processor = - XSLTProcessorFactory.getProcessor(new org.apache.xalan.xpath.xdom.XercesLiaison()); - StylesheetRoot theory_style1 = - theory_processor.processStylesheet(theory_xsl1); - theory_processor.reset(); - StylesheetRoot theory_style2 = - theory_processor.processStylesheet(theory_xsl2); - theory_processor.setStylesheet(theory_style2); - - XSLTProcessor processor = - XSLTProcessorFactory.getProcessor(new org.apache.xalan.xpath.xdom.XercesLiaison()); - StylesheetRoot style1 = processor.processStylesheet(xsl1); - processor.reset(); - StylesheetRoot style2 = processor.processStylesheet(xsl2); - processor.setStylesheet(style2); - - DatagramSocket socket = new DatagramSocket(port); - - System.out.println("Demon activated on input port " + port + - " and output port " + port2); - while(true) { - System.out.print("Ready..."); - - /* Warning: the packet must be a fresh one! */ - DatagramPacket packet = new DatagramPacket(new byte[1024],1024); - socket.receive(packet); - byte data[] = packet.getData(); - int datalen = packet.getLength(); - String received = new String(data,0,datalen); - - int first = received.indexOf(' '); - int last = received.lastIndexOf(' '); - String mode = received.substring(0,first); - String input = received.substring(first+1,last); - String output = received.substring(last+1); - - System.out.println("request received! Parameters are"); - System.out.println("Mode: " + mode + " "); - System.out.println("Input file: \"" + input + "\""); - System.out.println("Output file: \"" + output + "\"\n"); - - if ((new File(output)).exists()) { - System.out.println("Using cached version\n"); - } else { - FileOutputStream fout = new FileOutputStream(output); - if (mode.equals("cic")) { - processor.setDocumentHandler(style2.getSAXSerializer(fout)); - XSLTResultTarget content = new XSLTResultTarget(processor); - style1.process(new XSLTInputSource(input), content); - } else if (mode.equals("theory")) { - theory_processor.setDocumentHandler( - theory_style2.getSAXSerializer(fout)); - XSLTResultTarget content = - new XSLTResultTarget(theory_processor); - theory_style1.process(new XSLTInputSource(input), content); - } - } - - InetAddress address = InetAddress.getLocalHost(); - DatagramSocket socket2 = new DatagramSocket(); - - byte buf[] = new byte[0]; - DatagramPacket packet2 = new DatagramPacket(buf,0,address,port2); - - socket2.send(packet2); - } - } -} diff --git a/helm/interface/xaland-java/xaland.java.prima_del_loro_baco b/helm/interface/xaland-java/xaland.java.prima_del_loro_baco deleted file mode 100644 index b46ffa6aa..000000000 --- a/helm/interface/xaland-java/xaland.java.prima_del_loro_baco +++ /dev/null @@ -1,85 +0,0 @@ -import org.apache.xalan.xslt.*; -import java.net.*; -import java.io.*; - -public class xaland { - public static void Transform(StylesheetRoot style, String xmlSourceURL, String OutputURL) throws java.io.IOException, java.net.MalformedURLException, org.xml.sax.SAXException - { - XSLTInputSource xmlSource = new XSLTInputSource (xmlSourceURL); - XSLTResultTarget xmlResult = new XSLTResultTarget (OutputURL); - style.process(xmlSource, xmlResult); - } - - public static void main(String argv[]) throws java.io.IOException, java.net.MalformedURLException, org.xml.sax.SAXException - { - int port = Integer.parseInt(argv[0]); - int port2 = Integer.parseInt(argv[1]); - String xsl1 = argv[2]; - String xsl2 = argv[3]; - String theory_xsl1 = argv[4]; - String theory_xsl2 = argv[5]; - - XSLTProcessor theory_processor = XSLTProcessorFactory.getProcessor(); - StylesheetRoot theory_style1 = - theory_processor.processStylesheet(theory_xsl1); - StylesheetRoot theory_style2 = - theory_processor.processStylesheet(theory_xsl2); - theory_processor.setStylesheet(theory_style2); - - XSLTProcessor processor = XSLTProcessorFactory.getProcessor(); - StylesheetRoot style1 = processor.processStylesheet(xsl1); - StylesheetRoot style2 = processor.processStylesheet(xsl2); - processor.setStylesheet(style2); - - DatagramSocket socket = new DatagramSocket(port); - - System.out.println("Demon activated on input port " + port + - " and output port " + port2); - while(true) { - System.out.print("Ready..."); - - /* Warning: the packet must be a fresh one! */ - DatagramPacket packet = new DatagramPacket(new byte[1024],1024); - socket.receive(packet); - byte data[] = packet.getData(); - int datalen = packet.getLength(); - String received = new String(data,0,datalen); - - int first = received.indexOf(' '); - int last = received.lastIndexOf(' '); - String mode = received.substring(0,first); - String input = received.substring(first+1,last); - String output = received.substring(last+1); - - System.out.println("request received! Parameters are"); - System.out.println("Mode: " + mode + " "); - System.out.println("Input file: \"" + input + "\""); - System.out.println("Output file: \"" + output + "\"\n"); - - if ((new File(output)).exists()) { - System.out.println("Using cached version\n"); - } else { - FileOutputStream fout = new FileOutputStream(output); - if (mode.equals("cic")) { - processor.setDocumentHandler(style2.getSAXSerializer(fout)); - XSLTResultTarget content = new XSLTResultTarget(processor); - style1.process(new XSLTInputSource(input), content); - } else if (mode.equals("theory")) { - theory_processor.setDocumentHandler( - theory_style2.getSAXSerializer(fout)); - XSLTResultTarget content = - new XSLTResultTarget(theory_processor); - theory_style1.process(new XSLTInputSource(input), content); - } - } - - InetAddress address = InetAddress.getLocalHost(); - DatagramSocket socket2 = new DatagramSocket(); - - byte buf[] = new byte[0]; - DatagramPacket packet2 = new DatagramPacket(buf,0,address,port2); - - socket2.send(packet2); - } - } -} diff --git a/helm/interface/xaland-java/xaland.java.prima_del_loro_baco_ma_dopo_i_reset b/helm/interface/xaland-java/xaland.java.prima_del_loro_baco_ma_dopo_i_reset deleted file mode 100644 index 1467cdd2e..000000000 --- a/helm/interface/xaland-java/xaland.java.prima_del_loro_baco_ma_dopo_i_reset +++ /dev/null @@ -1,87 +0,0 @@ -import org.apache.xalan.xslt.*; -import java.net.*; -import java.io.*; - -public class xaland { - public static void Transform(StylesheetRoot style, String xmlSourceURL, String OutputURL) throws java.io.IOException, java.net.MalformedURLException, org.xml.sax.SAXException - { - XSLTInputSource xmlSource = new XSLTInputSource (xmlSourceURL); - XSLTResultTarget xmlResult = new XSLTResultTarget (OutputURL); - style.process(xmlSource, xmlResult); - } - - public static void main(String argv[]) throws java.io.IOException, java.net.MalformedURLException, org.xml.sax.SAXException - { - int port = Integer.parseInt(argv[0]); - int port2 = Integer.parseInt(argv[1]); - String xsl1 = argv[2]; - String xsl2 = argv[3]; - String theory_xsl1 = argv[4]; - String theory_xsl2 = argv[5]; - - XSLTProcessor theory_processor = XSLTProcessorFactory.getProcessor(); - StylesheetRoot theory_style1 = - theory_processor.processStylesheet(theory_xsl1); - theory_processor.reset(); - StylesheetRoot theory_style2 = - theory_processor.processStylesheet(theory_xsl2); - theory_processor.setStylesheet(theory_style2); - - XSLTProcessor processor = XSLTProcessorFactory.getProcessor(); - StylesheetRoot style1 = processor.processStylesheet(xsl1); - processor.reset(); - StylesheetRoot style2 = processor.processStylesheet(xsl2); - processor.setStylesheet(style2); - - DatagramSocket socket = new DatagramSocket(port); - - System.out.println("Demon activated on input port " + port + - " and output port " + port2); - while(true) { - System.out.print("Ready..."); - - /* Warning: the packet must be a fresh one! */ - DatagramPacket packet = new DatagramPacket(new byte[1024],1024); - socket.receive(packet); - byte data[] = packet.getData(); - int datalen = packet.getLength(); - String received = new String(data,0,datalen); - - int first = received.indexOf(' '); - int last = received.lastIndexOf(' '); - String mode = received.substring(0,first); - String input = received.substring(first+1,last); - String output = received.substring(last+1); - - System.out.println("request received! Parameters are"); - System.out.println("Mode: " + mode + " "); - System.out.println("Input file: \"" + input + "\""); - System.out.println("Output file: \"" + output + "\"\n"); - - if ((new File(output)).exists()) { - System.out.println("Using cached version\n"); - } else { - FileOutputStream fout = new FileOutputStream(output); - if (mode.equals("cic")) { - processor.setDocumentHandler(style2.getSAXSerializer(fout)); - XSLTResultTarget content = new XSLTResultTarget(processor); - style1.process(new XSLTInputSource(input), content); - } else if (mode.equals("theory")) { - theory_processor.setDocumentHandler( - theory_style2.getSAXSerializer(fout)); - XSLTResultTarget content = - new XSLTResultTarget(theory_processor); - theory_style1.process(new XSLTInputSource(input), content); - } - } - - InetAddress address = InetAddress.getLocalHost(); - DatagramSocket socket2 = new DatagramSocket(); - - byte buf[] = new byte[0]; - DatagramPacket packet2 = new DatagramPacket(buf,0,address,port2); - - socket2.send(packet2); - } - } -} diff --git a/helm/interface/xaland.class b/helm/interface/xaland.class deleted file mode 100644 index 6871fda4b..000000000 Binary files a/helm/interface/xaland.class and /dev/null differ diff --git a/helm/style/annotatedcont.xsl b/helm/style/annotatedcont.xsl new file mode 100644 index 000000000..e97d08f2b --- /dev/null +++ b/helm/style/annotatedcont.xsl @@ -0,0 +1,73 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/annotatedpres.xsl b/helm/style/annotatedpres.xsl new file mode 100644 index 000000000..511f915f5 --- /dev/null +++ b/helm/style/annotatedpres.xsl @@ -0,0 +1,34 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/basic.xsl b/helm/style/basic.xsl new file mode 100644 index 000000000..148912aa1 --- /dev/null +++ b/helm/style/basic.xsl @@ -0,0 +1,253 @@ + + + + + + + + + + + + + + +http://localhost:8081/getciconly?uri= + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + $x + + + app + + $x + + + + + + + + + + + + + + + + + + + + + + + + + app + + + + + + + + + + + + + + + + app + + + + + + + + + x + + + + app + + x + + + + app + + x + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/content.xsl b/helm/style/content.xsl new file mode 100644 index 000000000..486c0a43f --- /dev/null +++ b/helm/style/content.xsl @@ -0,0 +1,277 @@ + + + + + + + + + + + + + + + + + + + + + + +http://localhost:8081/getciconly?uri= + + + + + + + + + + + + + + + + + + + + + + arrow + + + + prod + + + + + + + + + + + + + + + + + cast + + + + + + + + + + + + + + + + + + + + + + + + + letin + + + + + let + + + + + + + + + + + + + + + + + app + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + mutcase + + + + + + + + + + + + + + + app + + + + LAMBDA + + + + LAMBDA + + + + + + + + fix + + + + + + + + + cofix + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl new file mode 100644 index 000000000..f2d618274 --- /dev/null +++ b/helm/style/content_to_html.xsl @@ -0,0 +1,657 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +   + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + P + + : + + +
+ + + + . + + + + + + + P + + : + + . + + + + + + + + ( + + + +
+ + + + + ® + + + + ) + + + ( + + + ® + + ) + + + + + + + ( + + + + +
+ + + + + + + + ) + + + ( + + +   + + + ) + + + + + + + + + ( + + +
+ + + :> + + + + ) + + + ( + + :> + + ) + + + + + + + + + + + + Prop + + + Set + + + Type + + + + + < + + + + > + CASE + + + + OF + +
+ + + + + +    + + + | + + + + Þ + + + + + + + < + + > + CASE + + OF + + + + | + + + + Þ + + + + + + + + + + + FIX + + { + +
+ + + + + : + + + +
+ + + + := + + + + +
+ + + + } + + + FIX + + { + + + : + + := + + + + } + + + ; + + + + + + + + + + COFIX + + { +
+ + + + + + : + + + +
+ + + + := + + + + + +
+ + + + } + + + COFIX + + { + + + : + + := + + + + } + + + ; + + + + + + + + + + + + + + + + + + + + + + + l + + : + + +
+ + + + . + + + + + + + l + + : + + . + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+DEFINITION ()
+TYPE =
+ + + + + +
+BODY =
+ + + + + + +

+ + + + + + +

+AXIOM ()
+TYPE = + + +

+ + + + + + +

+UNFINISHED PROOF ()
+THESIS: + +
+CONJECTURES: + +
+ + + + : + + + + +
+PROOF: + + + +

+ + + + + + +

+ + + + + + INDUCTIVE DEFINITION + + + COINDUCTIVE DEFINITION + + + + + AND + + + () + [ + + + + : + + + + ]
+ OF ARITY + + +
+ BUILT FROM: + +
+ + + + + +    + + + | + + + + : + + + + + +

+ + + + + + +

+VARIABLE
+TYPE = + + +

+ + + + + + + + + + +

BEGIN OF SECTION

+ +

END OF SECTION

+ + + diff --git a/helm/style/html_init.xsl b/helm/style/html_init.xsl new file mode 100644 index 000000000..44d75fd0a --- /dev/null +++ b/helm/style/html_init.xsl @@ -0,0 +1,259 @@ + + + + + + + + + +http://localhost:8081/getciconly?uri= + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + + + + + + + + ) + + + ( + + + + + + + + + + + ) + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + ( + + + +
+ + + + + + + + - + + + + + ) + + + ( + + + + + + - + + + ) + + + + + + + + + + + + + + + + + + + Ø + + + + + + + + + + + + + + + + + + + + + + $ + + + : + + + +
+ + + + . + + + + + + + + + + $ + + + : + + . + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/html_reals.xsl b/helm/style/html_reals.xsl new file mode 100644 index 000000000..1f1750b2d --- /dev/null +++ b/helm/style/html_reals.xsl @@ -0,0 +1,234 @@ + + + + + + + + + +http://localhost:8081/getciconly?uri= + + + + + + + + + + + + + + + + + + + lim + + + + ® + + +
+ + + + + + + + + + + + + lim + + + + ® + + + + + + + + + + + + + + + + + + + + + + d + / + + d + + + + + + + + + + + + + + + + | + + + + | + + + + + + + + + + + + + + ! + + + + + + + + + + + (sqr + + + + ) + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + { + + + + , +
+ + + + + + + } + + + + + + + + + { + + , + + } + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/html_set.xsl b/helm/style/html_set.xsl new file mode 100644 index 000000000..ca38298d1 --- /dev/null +++ b/helm/style/html_set.xsl @@ -0,0 +1,463 @@ + + + + + + + + + +http://localhost:8081/getciconly?uri= + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + Î + + + + + ) + + + ( + + + + + + Î + + + ) + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + Ï + + + + ) + + + ( + + Ï + + ) + + + + + + + + + + + + + + + Æ + + + + + + + + + + { + + : + + +
+ + + + | + + + + } + + + { + + : + + | + + } + + + + + + + { + + + + + , +
+ + + + + + + + } + + + { + + + + + } + + + , + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + Ç + + + + + ) + + + ( + + + + + + Ç + + + ) + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + È + + + + + ) + + + ( + + + + + + È + + + ) + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + Í + + + + + ) + + + ( + + + + + + Í + + + ) + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + Ì + + + + + ) + + + ( + + + + + + Ì + + + ) + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + / + + + + + ) + + + ( + + + + + + / + + + ) + + + + + + + + + + + + | + + + + | + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/mml2mmlv1_0.xsl b/helm/style/mml2mmlv1_0.xsl new file mode 100644 index 000000000..063bfb8ca --- /dev/null +++ b/helm/style/mml2mmlv1_0.xsl @@ -0,0 +1,2011 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + i + + + + + + + + - + + + + + + + + + i + + + + + + + + / + + + + + + + + / + + + + + + + + Polar + + + + + + + + + + Polar + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ln + + + exp + + + arcsin + + + arccos + + + arctan + + + arcsec + + + arccsc + + + arccot + + + arcsinh + + + arccosh + + + arctanh + + + arcsech + + + arccsch + + + arccoth + + + sin + + + cos + + + tan + + + + + + -1 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Λ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + id + + + + + + + + + + + + / + + + + + + + + + + e + + + + + + + + + + + + ! + + + + + + + + + + max + + + min + + + + + + + + + + + | + + + + + + + + + + + + + + max + + + min + + + + + + + + + | + + + + + + + max + + + min + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + % + + + / + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + * + + + + + + + + + + + + + + + + + + + + + 2 + + + + + + + + + gcd + + + + gcd + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + not + + + + + + + + + + for all + + + + + + + : + + , + + + + + + + + + + + + + + + + , + + + : + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + arg + + + Real + + + Imaginary + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + = + + + > + + + < + + + + + + + + + + + + + + + + + + + + + + + + + + ln + + + + + ln + + + + + + + + + + + + + + + + log + + + + + + log + + + + + + + + log + + + + log + + + + + + + + + + + + + + + + + + + + + + + + + d + + + + d + + + + + + + + + + d + + d + + + + + + + + + + + + + + + + d + + + + d + + + + + + + + + + d + + d + + + + + + + + + + + + + + + + + + div + + + grad + + + curl + + + + + + + + + + + + + + + + + + + Δ + 2 + + + + + + + + + + + + + + | + + + + + + + + + | + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + \ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + = + + + + + + + + + + + + + + + + + + + + + + + + + + + lim + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + sin + + + cos + + + tan + + + sec + + + csc + + + cot + + + sinh + + + cosh + + + tanh + + + sech + + + csch + + + coth + + + arcsin + + + arccos + + + arctan + + + + + + + + + + + + + + + + + + + + σ + + + + + + + + + + + + σ + + + + + + + 2 + + + + + + + + median + + + + + + + + + + + + mode + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + det + + + + + + + + T + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + . + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl new file mode 100644 index 000000000..0a11b4991 --- /dev/null +++ b/helm/style/mmlextension.xsl @@ -0,0 +1,1389 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + type="text/xhtml" + + + + + + + + + + + + DEFINITION () OF TYPE + + + + + + + __ + + + + + + + + AS + + + + + + + __ + + + + + + + + + + + + + + + + + AXIOM () OF TYPE + + + + + + + __ + + + + + + + + + + + + + + + + + UNFINISHED PROOF () + + + + + + + THESIS: + + + + + + + __ + + + + + + + + CONJECTURES: + + + + + + + + __ + : + + + + + + + + + CORRESPONDING PROOF: + + + + + + + __ + + + + + + + + + + + + + + + + + + + + + + INDUCTIVE DEFINITION + + + COINDUCTIVE DEFINITION + + + + + AND + + + _ + () + + + + + + + __ + [ + + + + + + + + + : + + + + + + + + + ] + + + + + + + ] + + + + + + + + + OF ARITY + + + + + + + __ + + + + + + + + BUILT FROM + + + + + + + + + + __ + + + | + _ + + + OF + _ + + + + + + + + + + + + + + + + + + + VARIABLE OF TYPE + + + + + + + __ + + + + + + + + + + + + + + + + + + + + + + + + + : + + + + + + + + + + + + : + + + + + + + + + + + + + + + + + + + + + + + + + + + + Π + + + + + + + . + + + + + + + + Π + + : + + . + + + + + + + + + + + + ( + + + + + + + + → + + + + + + + + ) + + + + + + + ( + + → + + ) + + + + + + + + + + + ( + + + + + + + + + ( + + + + + + + + + ) + + + + + + + ( + + + _ + + + ) + + + + + + + + + + + ( + + + + + + + + :> + + + + + + + + ) + + + + + + + ( + + :> + + ) + + + + + Prop + + + Set + + + Type + + + + + + + + + + < + + + > + CASES + _ + + + + + + + + + + > + CASES + _ + + + + + + + + + OF + + + + + + + + + + + | + + + | + + + _ + + + ⇒ + + + + + + + + + + |_ + ⇒ + + + + + + + + + + END + + + + + + + <> + CASES + _ + + _ + OF + + + + | + + + + ⇒ + + + _ + END + + + + + + + + + + + FIX + _ + + { + + + + + + + __ + + + + + + + + : + + + + + + + + + + + := + + + + + + + + + := + + + + + + + + + + + + + } + + + + + + + FIX + + { + + + + + + + : + + := + + + } + + + + + + + + + + + + + + + + + COFIX + _ + + { + + + + + + + __ + + + + + + + + : + + + + + + + + + + + := + + + + + + + + + := + + + + + + + + + + + + + } + + + + + + + COFIX + + { + + + + + + + : + + := + + + } + + + + + + + + + + + + + + + + + + + + + + + + + we proved + _ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + ) + + + + + + + + + + + + + Consider + + + + + + + + + + + + + + + Rewrite + _ + + _ + with + _ + + _ + by + _ + + _ + in + _ + + _ + and apply to + _ + + + + + + + + + + + + + + + + + Consider + + + + + + + + + In particular, we have + + + + + + ( + + ) + _ + + + + + + + + ( + + ) + _ + + + + + + + + + + + + + + + + + + + + + + + + Consider + _ + + + + + + + + + We prove + _ + + _ + by cases: + + + + + + * + + + + + + + + * + + + + + + + + ERROR + + + + + + + + + + + + + Rewrite + _ + + _ + with + _ + + _ + by + _ + + + + + + + + we get + _ + + + + + + + + + + + + + + + + + we get + _ + + + + + + + + + + + + + + + + + + + + + λ + + + + + + + . + + + + + + + + λ + + : + + . + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + + + + + __ + + = + + + + + + + + ) + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + + + + + __ + + + + + + + + + + ) + + + + + + + + + + + + + + + + + + + + + + + + + + + + + { + + + + + + { + | + + + + + + } + + + + + + + + + { + + + , + + + + + + + { + + + , + + + + + + + } + + + + + + + + + + + + + + + + | + + | + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + > + + + + + + + + + + + diff --git a/helm/style/objcontent.xsl b/helm/style/objcontent.xsl new file mode 100644 index 000000000..112e73ab1 --- /dev/null +++ b/helm/style/objcontent.xsl @@ -0,0 +1,232 @@ + + + + + + + + + + + + + + + + + + + + + type="text/xml" + href="" type="text/xsl" + type="xslt" + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +PROD + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + app + + + + + + + + + + + + + + + + + + + + + + + + + + $ + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/params.xsl b/helm/style/params.xsl new file mode 100644 index 000000000..dc59df167 --- /dev/null +++ b/helm/style/params.xsl @@ -0,0 +1,243 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 0 + + + + + + + + + + + + + + + + + + + + + + + + 0 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl new file mode 100644 index 000000000..cd7593052 --- /dev/null +++ b/helm/style/proofs.xsl @@ -0,0 +1,255 @@ + + + + + + + + + + + + + + +http://localhost:8081/getciconly?uri= + + + + + + + + + + + + + + + + + + thread + + + rw_step + + + + + + + + + + + and_ind + + + + + + + + + + + or_ind + + + + + + + + + thread + + + app + + + + + + + + proof + + + + + + + + + + + + + + + + + + + + + + previous + + + + + + + + + + + + + + + rw_step + + + + + + + + + + + + + + + thread + + + app + + + + + + + + + + + + + + + + + + + + + + + + + rewrite_and_apply + + rw_step + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + app + + + + + + + + + + + app + + * + * + * + + + + + + app + + + + + + + + + + + + + + diff --git a/helm/style/reals.xsl b/helm/style/reals.xsl new file mode 100644 index 000000000..ff69f9a22 --- /dev/null +++ b/helm/style/reals.xsl @@ -0,0 +1,277 @@ + + + + + + + + + + + + + + +http://localhost:8081/getciconly?uri= + + + + + + + + + + + 0 + + + + 1 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 1 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + $x + + + + + + app + + $x + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + $x + + + app + + $x + + + + + + + + + + + + + + diff --git a/helm/style/ricerca.xsl b/helm/style/ricerca.xsl new file mode 100644 index 000000000..28e210dca --- /dev/null +++ b/helm/style/ricerca.xsl @@ -0,0 +1,91 @@ + + + + + + + + + + + + +http://localhost:8081/getciconly?uri= + + + + + + + + + + + + + + + + + + + +
+ + + + + + + + + + + + + + + + +
+ + + + + + + + + + +
+ + + + + + + + +
+ + + + + + + + + + + + + diff --git a/helm/style/rootcontent.xsl b/helm/style/rootcontent.xsl new file mode 100644 index 000000000..e82a13d63 --- /dev/null +++ b/helm/style/rootcontent.xsl @@ -0,0 +1,30 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/roottheory.xsl b/helm/style/roottheory.xsl new file mode 100644 index 000000000..5ba277e8d --- /dev/null +++ b/helm/style/roottheory.xsl @@ -0,0 +1,25 @@ + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/set.xsl b/helm/style/set.xsl new file mode 100644 index 000000000..916a92c51 --- /dev/null +++ b/helm/style/set.xsl @@ -0,0 +1,472 @@ + + + + + + + + + + + + + + +http://localhost:8081/getciconly?uri= + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/annotatedcont.xsl b/helm/style/style_prima_del_linguaggio_naturale/annotatedcont.xsl new file mode 100644 index 000000000..e97d08f2b --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/annotatedcont.xsl @@ -0,0 +1,73 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/annotatedpres.xsl b/helm/style/style_prima_del_linguaggio_naturale/annotatedpres.xsl new file mode 100644 index 000000000..511f915f5 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/annotatedpres.xsl @@ -0,0 +1,34 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/basic.xsl b/helm/style/style_prima_del_linguaggio_naturale/basic.xsl new file mode 100644 index 000000000..3f5422a72 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/basic.xsl @@ -0,0 +1,253 @@ + + + + + + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + $x + + + app + + $x + + + + + + + + + + + + + + + + + + + + + + + + + app + + + + + + + + + + + + + + + + app + + + + + + + + + x + + + + app + + x + + + + app + + x + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/content.xsl b/helm/style/style_prima_del_linguaggio_naturale/content.xsl new file mode 100644 index 000000000..7de998720 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/content.xsl @@ -0,0 +1,215 @@ + + + + + + + + + + + + + + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + + + + + + + + + + + + arrow + + + + prod + + + + + + + + + + + + + + + + + cast + + + + + + + + + + + + + + + + + + + + + app + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + mutcase + + + + + + + + + + + + + + + app + + + + LAMBDA + + + + LAMBDA + + + + + + + + fix + + + + + + + + + cofix + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/content_to_html.xsl b/helm/style/style_prima_del_linguaggio_naturale/content_to_html.xsl new file mode 100644 index 000000000..dd1c07794 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/content_to_html.xsl @@ -0,0 +1,657 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +   + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + P + + : + + +
+ + + + . + + + + + + + P + + : + + . + + + + + + + + ( + + + +
+ + + + + ® + + + + ) + + + ( + + + ® + + ) + + + + + + + ( + + + + +
+ + + + + + + + ) + + + ( + + +   + + + ) + + + + + + + + + ( + + +
+ + + :> + + + + ) + + + ( + + :> + + ) + + + + + + + + + + + + Prop + + + Set + + + Type + + + + + < + + + + > + CASE + + + + OF + +
+ + + + + +    + + + | + + + + Þ + + + + + + + < + + > + CASE + + OF + + + + | + + + + Þ + + + + + + + + + + + FIX + + { + +
+ + + + + : + + + +
+ + + + := + + + + +
+ + + + } + + + FIX + + { + + + : + + := + + + + } + + + ; + + + + + + + + + + COFIX + + { +
+ + + + + + : + + + +
+ + + + := + + + + + +
+ + + + } + + + COFIX + + { + + + : + + := + + + + } + + + ; + + + + + + + + + + + + + + + + + + + + + + + l + + : + + +
+ + + + . + + + + + + + l + + : + + . + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+DEFINITION ()
+TYPE =
+ + + + + +
+BODY =
+ + + + + + +

+ + + + + + +

+AXIOM ()
+TYPE = + + +

+ + + + + + +

+UNFINISHED PROOF ()
+THESIS: + +
+CONJECTURES: + +
+ + + + : + + + + +
+PROOF: + + + +

+ + + + + + +

+ + + + + + INDUCTIVE DEFINITION + + + COINDUCTIVE DEFINITION + + + + + AND + + + () + [ + + + + : + + + + ]
+ OF ARITY + + +
+ BUILT FROM: + +
+ + + + + +    + + + | + + + + : + + + + + +

+ + + + + + +

+VARIABLE
+TYPE = + + +

+ + + + + + + + + + +

BEGIN OF SECTION

+ +

END OF SECTION

+ + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/html_init.xsl b/helm/style/style_prima_del_linguaggio_naturale/html_init.xsl new file mode 100644 index 000000000..9e81b169c --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/html_init.xsl @@ -0,0 +1,259 @@ + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + + + + + + + + ) + + + ( + + + + + + + + + + + ) + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + ( + + + +
+ + + + + + + + - + + + + + ) + + + ( + + + + + + - + + + ) + + + + + + + + + + + + + + + + + + + Ø + + + + + + + + + + + + + + + + + + + + + + $ + + + : + + + +
+ + + + . + + + + + + + + + + $ + + + : + + . + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/html_reals.xsl b/helm/style/style_prima_del_linguaggio_naturale/html_reals.xsl new file mode 100644 index 000000000..04ff478c5 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/html_reals.xsl @@ -0,0 +1,234 @@ + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + + + + + + + + + lim + + + + ® + + +
+ + + + + + + + + + + + + lim + + + + ® + + + + + + + + + + + + + + + + + + + + + + d + / + + d + + + + + + + + + + + + + + + + | + + + + | + + + + + + + + + + + + + + ! + + + + + + + + + + + (sqr + + + + ) + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + { + + + + , +
+ + + + + + + } + + + + + + + + + { + + , + + } + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/html_set.xsl b/helm/style/style_prima_del_linguaggio_naturale/html_set.xsl new file mode 100644 index 000000000..6c7f66b1b --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/html_set.xsl @@ -0,0 +1,463 @@ + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + Î + + + + + ) + + + ( + + + + + + Î + + + ) + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + Ï + + + + ) + + + ( + + Ï + + ) + + + + + + + + + + + + + + + Æ + + + + + + + + + + { + + : + + +
+ + + + | + + + + } + + + { + + : + + | + + } + + + + + + + { + + + + + , +
+ + + + + + + + } + + + { + + + + + } + + + , + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + Ç + + + + + ) + + + ( + + + + + + Ç + + + ) + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + È + + + + + ) + + + ( + + + + + + È + + + ) + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + Í + + + + + ) + + + ( + + + + + + Í + + + ) + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + Ì + + + + + ) + + + ( + + + + + + Ì + + + ) + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + / + + + + + ) + + + ( + + + + + + / + + + ) + + + + + + + + + + + + | + + + + | + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/mml2mmlv1_0.xsl b/helm/style/style_prima_del_linguaggio_naturale/mml2mmlv1_0.xsl new file mode 100644 index 000000000..67e1accfb --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/mml2mmlv1_0.xsl @@ -0,0 +1,1957 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + i + + + + + + + + - + + + + + + + + + i + + + + + + + + / + + + + + + + + / + + + + + + + + Polar + + + + + + + + + + Polar + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ln + + + exp + + + arcsin + + + arccos + + + arctan + + + arcsec + + + arccsc + + + arccot + + + arcsinh + + + arccosh + + + arctanh + + + arcsech + + + arccsch + + + arccoth + + + sin + + + cos + + + tan + + + + + + -1 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Λ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + id + + + + + + + + + + + + / + + + + + + + + + + e + + + + + + + + + + + + ! + + + + + + + + + + max + + + min + + + + + + + + + + + | + + + + + + + + + + + + + + max + + + min + + + + + + + + + | + + + + + + + max + + + min + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + % + + + / + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + * + + + + + + + + + + + + + + + + + + + + + 2 + + + + + + + + + gcd + + + + gcd + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + not + + + + + + + + + + for all + + + + + + + : + + , + + + + + + + + + + + + + + + + , + + + : + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + arg + + + Real + + + Imaginary + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + = + + + > + + + < + + + + + + + + + + + + + + + + + + + + + + + + + + ln + + + + + ln + + + + + + + + + + + + + + + + log + + + + + + log + + + + + + + + log + + + + log + + + + + + + + + + + + + + + + + + + + + + + + + d + + + + d + + + + + + + + + + d + + d + + + + + + + + + + + + + + + + d + + + + d + + + + + + + + + + d + + d + + + + + + + + + + + + + + + + + + div + + + grad + + + curl + + + + + + + + + + + + + + + + + + + Δ + 2 + + + + + + + + + + + + + + | + + + + + + + + + | + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + \ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + = + + + + + + + + + + + + + + + + + + + + + + + + + + + lim + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + sin + + + cos + + + tan + + + sec + + + csc + + + cot + + + sinh + + + cosh + + + tanh + + + sech + + + csch + + + coth + + + arcsin + + + arccos + + + arctan + + + + + + + + + + + + + + + + + + + + σ + + + + + + + + + + + + σ + + + + + + + 2 + + + + + + + + median + + + + + + + + + + + + mode + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + det + + + + + + + + T + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + . + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/mml2mmlv1_0_original.xsl b/helm/style/style_prima_del_linguaggio_naturale/mml2mmlv1_0_original.xsl new file mode 100644 index 000000000..44c34df74 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/mml2mmlv1_0_original.xsl @@ -0,0 +1,1848 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + i + + + + + + + + - + + + + + + + + + i + + + + + + + + / + + + + + + + + / + + + + + + + + Polar + + + + + + + + + + Polar + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ln + + + exp + + + arcsin + + + arccos + + + arctan + + + arcsec + + + arccsc + + + arccot + + + arcsinh + + + arccosh + + + arctanh + + + arcsech + + + arccsch + + + arccoth + + + sin + + + cos + + + tan + + + + + + -1 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Λ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + id + + + + + + + + + + + / + + + + + + + + + + e + + + + + + + + + + + ! + + + + + + + + + max + + + min + + + + + + + + + + + | + + + + + + + + + + + + + + max + + + min + + + + + + + + + | + + + + + + + max + + + min + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + % + + + / + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 2 + + + + + + + + gcd + + + + gcd + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + not + + + + + + + + + for all + + + + + + + : + + , + + + + + + + + + + + + + + + , + + + : + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + arg + + + Real + + + Imaginary + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + = + + + > + + + < + + + + + + + + + + + + + + + + + + + + + + + + + ln + + + + + ln + + + + + + + + + + + + + + + log + + + + + + log + + + + + + + + log + + + + log + + + + + + + + + + + + + + + + + + + + + + + + d + + + + d + + + + + + + + + + d + + d + + + + + + + + + + + + + + + d + + + + d + + + + + + + + + + d + + d + + + + + + + + + + + + + + + + + div + + + grad + + + curl + + + + + + + + + + + + + + + + + + Δ + 2 + + + + + + + + + + + + + | + + + + + + + + + | + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + \ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + = + + + + + + + + + + + + + + + + + + + + + + + + + + lim + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + sin + + + cos + + + tan + + + sec + + + csc + + + cot + + + sinh + + + cosh + + + tanh + + + sech + + + csch + + + coth + + + arcsin + + + arccos + + + arctan + + + + + + + + + + + + + + + + + + σ + + + + + + + + + + + σ + + + + + + + 2 + + + + + + + median + + + + + + + + + + + mode + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + det + + + + + + + + T + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + . + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/mmlextension.xsl b/helm/style/style_prima_del_linguaggio_naturale/mmlextension.xsl new file mode 100644 index 000000000..39d2f5c47 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/mmlextension.xsl @@ -0,0 +1,1128 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + type="text/xhtml" + + + + + + + + + + + + DEFINITION () OF TYPE + + + + + + + __ + + + + + + + + AS + + + + + + + __ + + + + + + + + + + + + + + + + + AXIOM () OF TYPE + + + + + + + __ + + + + + + + + + + + + + + + + + UNFINISHED PROOF () + + + + + + + THESIS: + + + + + + + __ + + + + + + + + CONJECTURES: + + + + + + + + __ + : + + + + + + + + + CORRESPONDING PROOF: + + + + + + + __ + + + + + + + + + + + + + + + + + + + + + + INDUCTIVE DEFINITION + + + COINDUCTIVE DEFINITION + + + + + AND + + + _ + () + + + + + + + __ + [ + + + + + + + + + : + + + + + + + + + ] + + + + + + + ] + + + + + + + + + OF ARITY + + + + + + + __ + + + + + + + + BUILT FROM + + + + + + + + + + __ + + + | + _ + + + OF + _ + + + + + + + + + + + + + + + + + + + VARIABLE OF TYPE + + + + + + + __ + + + + + + + + + + + + + + + + + + + + + + + + + : + + + + + + + + + + + + : + + + + + + + + + + + + + + + + + + + + + + + + + + + + Π + + + + + + + . + + + + + + + + Π + + : + + . + + + + + + + + + + + + ( + + + + + + + + → + + + + + + + + ) + + + + + + + ( + + → + + ) + + + + + + + + + + + ( + + + + + + + + + ( + + + + + + + + + ) + + + + + + + ( + + + _ + + + ) + + + + + + + + + + + ( + + + + + + + + :> + + + + + + + + ) + + + + + + + ( + + :> + + ) + + + + + Prop + + + Set + + + Type + + + + + + + + + + < + + + > + CASES + _ + + + + + + + + + + > + CASES + _ + + + + + + + + + OF + + + + + + + + + + + | + + + | + + + _ + + + ⇒ + + + + + + + + + + |_ + ⇒ + + + + + + + + + + END + + + + + + + <> + CASES + _ + + _ + OF + + + + | + + + + ⇒ + + + _ + END + + + + + + + + + + + FIX + _ + + { + + + + + + + __ + + + + + + + + : + + + + + + + + + + + := + + + + + + + + + := + + + + + + + + + + + + + } + + + + + + + FIX + + { + + + + + + + : + + := + + + } + + + + + + + + + + + + + + + + + COFIX + _ + + { + + + + + + + __ + + + + + + + + : + + + + + + + + + + + := + + + + + + + + + := + + + + + + + + + + + + + } + + + + + + + COFIX + + { + + + + + + + : + + := + + + } + + + + + + + + + + + + + + + + + + + + + + + + λ + + + + + + + . + + + + + + + + λ + + : + + . + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + + + + + __ + + = + + + + + + + + ) + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + + + + + __ + + + + + + + + + + ) + + + + + + + + + + + + + + + + + + + + + + + + + + + + + { + + + + + + { + | + + + + + + } + + + + + + + + + { + + + , + + + + + + + { + + + , + + + + + + + } + + + + + + + + + + + + + + + + | + + | + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + > + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/objcontent.xsl b/helm/style/style_prima_del_linguaggio_naturale/objcontent.xsl new file mode 100644 index 000000000..6ad0a4922 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/objcontent.xsl @@ -0,0 +1,232 @@ + + + + + + + + + + + + + + + + + + + + + type="text/xml" + href="" type="text/xsl" + type="xslt" + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +PROD + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + app + + + + + + + + + + + + + + + + + + + + + + + + + + $ + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/params.xsl b/helm/style/style_prima_del_linguaggio_naturale/params.xsl new file mode 100644 index 000000000..034eeba97 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/params.xsl @@ -0,0 +1,191 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 0 + + + + + + + + + + + + + + + + + + + + + + + + 0 + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/reals.xsl b/helm/style/style_prima_del_linguaggio_naturale/reals.xsl new file mode 100644 index 000000000..0e4afef94 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/reals.xsl @@ -0,0 +1,277 @@ + + + + + + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + 0 + + + + 1 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 1 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + $x + + + + + + app + + $x + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + $x + + + app + + $x + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/ricerca.xsl b/helm/style/style_prima_del_linguaggio_naturale/ricerca.xsl new file mode 100644 index 000000000..e0fa13a93 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/ricerca.xsl @@ -0,0 +1,91 @@ + + + + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + + + + + + + + + +
+ + + + + + + + + + + + + + + + +
+ + + + + + + + + + +
+ + + + + + + + +
+ + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/rootcontent.xsl b/helm/style/style_prima_del_linguaggio_naturale/rootcontent.xsl new file mode 100644 index 000000000..2a680a435 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/rootcontent.xsl @@ -0,0 +1,26 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/roottheory.xsl b/helm/style/style_prima_del_linguaggio_naturale/roottheory.xsl new file mode 100644 index 000000000..d293ee6f2 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/roottheory.xsl @@ -0,0 +1,22 @@ + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/set.xsl b/helm/style/style_prima_del_linguaggio_naturale/set.xsl new file mode 100644 index 000000000..303c872ef --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/set.xsl @@ -0,0 +1,487 @@ + + + + + + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/theory_content.xsl b/helm/style/style_prima_del_linguaggio_naturale/theory_content.xsl new file mode 100644 index 000000000..9b65cc5b2 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/theory_content.xsl @@ -0,0 +1,57 @@ + + + + + + + + + + + + + + + +http://localhost:8081/get?url= + + + + +
+ +
+ + + + + + +
+ +
+ + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/theory_pres.xsl b/helm/style/style_prima_del_linguaggio_naturale/theory_pres.xsl new file mode 100644 index 000000000..9a96cdc03 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/theory_pres.xsl @@ -0,0 +1,34 @@ + + + + + + + + + + + + + + + + + + + BEGIN SECTION + + END SECTION + + + + + BEGIN SECTION + + END SECTION + + + + + diff --git a/helm/style/theory_content.xsl b/helm/style/theory_content.xsl new file mode 100644 index 000000000..5ff5a41f7 --- /dev/null +++ b/helm/style/theory_content.xsl @@ -0,0 +1,57 @@ + + + + + + + + + + + + + + + +http://localhost:8081/getciconly?uri= + + + + +
+ +
+ + + + + + +
+ +
+ + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/theory_pres.xsl b/helm/style/theory_pres.xsl new file mode 100644 index 000000000..f8ade2a82 --- /dev/null +++ b/helm/style/theory_pres.xsl @@ -0,0 +1,35 @@ + + + + + + + + + + + + + + + + + + + + BEGIN SECTION + + END SECTION + + + + + BEGIN SECTION + + END SECTION + + + + +