From: Luca Padovani Date: Fri, 4 Apr 2003 13:41:22 +0000 (+0000) Subject: * the documents passed to the ocaml binding have been turned into strings X-Git-Tag: before_refactoring~50 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dbc6a4fb0236cfc7752c70e2e16f511b9e51b29c;p=helm.git * the documents passed to the ocaml binding have been turned into strings so that the relative uri resolution mechanism implemented in the TDictionary class can be effectively used --- diff --git a/helm/DEVEL/mathml_editor/doc/spec.tex b/helm/DEVEL/mathml_editor/doc/spec.tex index be9ba51bb..7849651d9 100644 --- a/helm/DEVEL/mathml_editor/doc/spec.tex +++ b/helm/DEVEL/mathml_editor/doc/spec.tex @@ -200,22 +200,23 @@ The following tokens are defined: \begin{table} \[ \begin{array}{rcl@{\hspace{3em}}rcl@{\hspace{3em}}rcl} - C &::=& Q\verb+/+ & Q &::=& T & P &::=& P' \\ - &|& Q\verb+//+ & &|& Q\verb+[@+n\verb+=+v\verb+]+ & &|& \verb+^+P'\\ - &|& \verb+(+C\verb+)+ & &|& Q\verb+[!@+n\verb+=+v\verb+]+ & &|& P'\verb+$+\\%$ - &|& (\alpha\verb+=+C) & &|& Q\verb+[@+n\verb+]+ & &|& \verb+^+P'\verb+$+\\%$ - &|& C_1 \verb+&+ C_2 & &|& Q\verb+[+P\verb+]+ & & &\\ - &|& C_1 \verb+|+ C_2 & & & & P' &::=& P''\\ - &|& C\verb.+. & T &::=& N & &|& P''\verb+#+P''\\ - &|& C\verb+*+ & &|& C N & & &\\ - &|& C\verb+?+ & & & & P'' &::=& \\ - &|& C_1~C_2 & N &::=& \verb+<*>+ & &|& T\;P''\\ - &|& \verb+!+C & &|& \verb+<+n_1\verb+|+\cdots\verb+|+n_2\verb+>+ & & &\\ - & & & &|& \verb++ & & &\\ + C &::=& . & Q &::=& \langle*\rangle & P &::=& P'\#P' \\ + &|& .. & &|& \langle!*\rangle & &|& \cent P'\#P'\\ + &|& / & &|& \langle n_1\mid\cdots\mid n_k\rangle & &|& P'\#P'\$\\%$ + &|& Q & &|& \langle!n_1\mid\cdots\mid n_k\rangle & &|& \cent P'\#P'\$\\%$ + &|& (C) & &|& Q[@n] & & &\\ + &|& \{C:\Gamma\} & &|& Q[!@n] & P' &::=& \\ + &|& C\&C & &|& Q[@n=v] & &|& C\;P'\\ + &|& C\mid C & &|& Q[!@n=v] & & &\\ + &|& C+ & &|& Q[P] & & &\\ + &|& C? & &|& Q[!P] & & &\\ + &|& C* & & & & & &\\ + &|& C\;C & & & & & &\\ + &|& !C & & & & & &\\ \end{array} \] -\caption{Syntax of the pattern language. $n$, $n_i$ denote names, $v$ -denotes a string enclosed in single or double quotes} +\caption{Syntax of the regular context language. $n$, $n_i$ denote +names, $v$ denotes a string enclosed in single or double quotes} \end{table} @@ -872,13 +873,14 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node \CSEM{/}{x} &=& \CHILDREN{x}\\ \CSEM{q}{x} &=& \{x_1\mid x_1\in\{x\} \wedge \QSEM{q}{x_1}\}\\ \CSEM{(c)}{x} &=& \CSEM{c}{x}\\ - \CSEM{\alpha(c)}{x} &=& \CSEM{c}{x}, \mbox{bind $\alpha$ to $x$}\\ + \CSEM{\{c:\alpha\}}{x} &=& \alpha(x,\CSEM{c}{x})\\ \CSEM{c_1\&c_2}{x} &=& \CSEM{c_1}{x} \cap \CSEM{c_2}{x}\\ \CSEM{c_1\mid c_2}{x} &=& \CSEM{c_1}{x} \cup \CSEM{c_2}{x}\\ \CSEM{c+}{x} &=& \CSEM{c}{x} \cup \CSEM{c+}{\CSEM{c}{x}}\\ \CSEM{c?}{x} &=& \CSEM{.\mid c}{x}\\ \CSEM{c*}{x} &=& \CSEM{{c+}?}{x}\\ - \CSEM{c_1\;c_2}{x} &=& \CSEM{c_2}{\CSEM{c_1}{x}}\\[3ex] + \CSEM{c_1\;c_2}{x} &=& \CSEM{c_2}{\CSEM{c_1}{x}}\\ + \CSEM{!c}{x} &=& \{x_1\mid x_1\in\{x\} \wedge \CSEM{c}{x}=\emptyset\}\\[3ex] \QSEM{\langle*\rangle}{x} &=& \ISELEMENT{x}\\ \QSEM{\langle!*\rangle}{x} &=& \neg\QSEM{\langle*\rangle}{x}\\ \QSEM{\langle n_1\mid\cdots\mid n_k\rangle}{x} &=& \exists i\in\{1,\dots,k\}:\NAME{x}=n_i\\ @@ -889,16 +891,18 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node \QSEM{q[!@n=v]}{x} &=& \QSEM{q}{x} \wedge \ATTRIBUTE{x}{n}\ne v\\ \QSEM{q[p]}{x} &=& \QSEM{q}{x} \wedge \PSEM{p}{x}\\ \QSEM{q[!p]}{x} &=& \QSEM{q}{x} \wedge \neg\PSEM{p}{x}\\[3ex] - \PSEM{p_1\#p_2}{x} &=& \PPSEM{p_1}{*,x}\wedge\PPSEM{p_2}{x,*}\\ - \PSEM{\cent p_1\#p_2}{x} &=& \PPSEM{p_1}{\cent,x}\wedge\PPSEM{p_2}{x,*}\\ - \PSEM{p_1\#p_2\$}{x} &=& \PPSEM{p_1}{*,x}\wedge\PPSEM{p_2}{x,\$}\\ - \PSEM{\cent p_1\#p_2\$}{x} &=& \PPSEM{p_1}{\cent,x}\wedge\PPSEM{p_2}{x,\$}\\[3ex] - \PPSEM{}{*,x} &=& \mathit{true}\\ - \PPSEM{}{\cent,x} &=& \PREV{x}=\emptyset\\ - \PPSEM{}{x,*} &=& \mathit{true}\\ - \PPSEM{}{x,\$} &=& \NEXT{x}=\emptyset\\ - \PPSEM{p\;c}{\alpha,x} &=& \CSEM{c}{\PREV{x}}\ne\emptyset\wedge\PPSEM{p}{\alpha,\PREV{x}}\\ - \PPSEM{c\;p}{x,\alpha} &=& \CSEM{c}{\NEXT{x}}\ne\emptyset\wedge\PPSEM{p}{\NEXT{x},\alpha}\\ + \PSEM{p_1\#p_2}{x} &=& \PPSEM{p_1}{*,\PREV{x}}\wedge\PPSEM{p_2}{\NEXT{x},*}\\ + \PSEM{\cent p_1\#p_2}{x} &=& \PPSEM{p_1}{\cent,\PREV{x}}\wedge\PPSEM{p_2}{\NEXT{x},*}\\ + \PSEM{p_1\#p_2\$}{x} &=& \PPSEM{p_1}{*,\PREV{x}}\wedge\PPSEM{p_2}{\NEXT{x},\$}\\ + \PSEM{\cent p_1\#p_2\$}{x} &=& \PPSEM{p_1}{\cent,\PREV{x}}\wedge\PPSEM{p_2}{\NEXT{x},\$}\\[3ex] + \PPSEM{}{*,\alpha} &=& \mathit{true}\\ + \PPSEM{}{\cent,\alpha} &=& \alpha=\emptyset\\ + \PPSEM{p\;c}{\alpha,\emptyset} &=& \mathit{false}\\ + \PPSEM{p\;c}{\alpha,\{x\}} &=& \CSEM{c}{x}\ne\emptyset\wedge\PPSEM{p}{\alpha,\PREV{x}}\\ + \PPSEM{}{\alpha,*} &=& \mathit{true}\\ + \PPSEM{}{\alpha,\$} &=& \alpha=\emptyset\\ + \PPSEM{c\;p}{\emptyset,\alpha} &=& \mathit{false}\\ + \PPSEM{c\;p}{\{x\},\alpha} &=& \CSEM{c}{x}\ne\emptyset\wedge\PPSEM{p}{\NEXT{x},\alpha}\\ \end{array} \] diff --git a/helm/DEVEL/mathml_editor/ocaml/c_mathml_editor.cc b/helm/DEVEL/mathml_editor/ocaml/c_mathml_editor.cc index f610a7ff5..14bab319d 100644 --- a/helm/DEVEL/mathml_editor/ocaml/c_mathml_editor.cc +++ b/helm/DEVEL/mathml_editor/ocaml/c_mathml_editor.cc @@ -59,7 +59,7 @@ CCallbackLogger::message(Level l, const std::string& s) struct Editor { - Editor(const DOM::Document&, const DOM::Document&, const DOM::Document&, void (*)(int, const char*, void*), void*); + Editor(const char*, const char*, const char*, void (*)(int, const char*, void*), void*); ~Editor(); ALogger* logger; @@ -71,13 +71,19 @@ struct Editor APushLexer* lexer; }; -Editor::Editor(const DOM::Document& dict, const DOM::Document& mml, const DOM::Document& tex, +Editor::Editor(const char* dict_uri, const char* mml_uri, const char* tex_uri, void (*cb)(int, const char*, void*), void* data) { + assert(dict_uri); + assert(mml_uri); + assert(tex_uri); assert(cb); logger = new CCallbackLogger(cb, data); dictionary = new TDictionary(*logger); - dictionary->load(DOM::Document(dict)); + dictionary->load(dict_uri); + DOM::DOMImplementation di; + DOM::Document mml = di.createDocumentFromURI(mml_uri); + DOM::Document tex = di.createDocumentFromURI(tex_uri); tml_mml = new DOMX::XSLTStylesheet(mml); tml_tex = new DOMX::XSLTStylesheet(tex); factory = new CMathMLFactoryXSLT(*logger, *tml_mml); @@ -115,15 +121,13 @@ c_mathml_editor_get_default_tex_stylesheet_path() } extern "C" Editor* -c_mathml_editor_new(GdomeDocument* dictionary, - GdomeDocument* tml_mml, - GdomeDocument* tml_tex, +c_mathml_editor_new(const char* dictionary_uri, + const char* tml_mml_uri, + const char* tml_tex_uri, void (*log_message_cb)(int, const char*, void*), void* user_data) { - return new Editor(DOM::Document(dictionary), - DOM::Document(tml_mml), - DOM::Document(tml_tex), log_message_cb, user_data); + return new Editor(dictionary_uri, tml_mml_uri, tml_tex_uri, log_message_cb, user_data); } extern "C" void diff --git a/helm/DEVEL/mathml_editor/ocaml/c_mathml_editor.h b/helm/DEVEL/mathml_editor/ocaml/c_mathml_editor.h index 6c8a5f5cb..7c41ece31 100644 --- a/helm/DEVEL/mathml_editor/ocaml/c_mathml_editor.h +++ b/helm/DEVEL/mathml_editor/ocaml/c_mathml_editor.h @@ -33,7 +33,7 @@ typedef struct Editor Editor; const char* c_mathml_editor_get_default_dictionary_path(void); const char* c_mathml_editor_get_default_mathml_stylesheet_path(void); const char* c_mathml_editor_get_default_tex_stylesheet_path(void); -Editor* c_mathml_editor_new(GdomeDocument*, GdomeDocument*, GdomeDocument*, void (*)(int, const char*, void*), void*); +Editor* c_mathml_editor_new(const char*, const char*, const char*, void (*)(int, const char*, void*), void*); void c_mathml_editor_destroy(Editor*); int c_mathml_editor_freeze(Editor*); int c_mathml_editor_thaw(Editor*); diff --git a/helm/DEVEL/mathml_editor/ocaml/i_mathml_editor.ml b/helm/DEVEL/mathml_editor/ocaml/i_mathml_editor.ml index 25171b8bb..c98c2fbe1 100644 --- a/helm/DEVEL/mathml_editor/ocaml/i_mathml_editor.ml +++ b/helm/DEVEL/mathml_editor/ocaml/i_mathml_editor.ml @@ -35,9 +35,9 @@ external get_default_tex_stylesheet_path : unit -> string = "ml_mathml_editor_get_default_tex_stylesheet_path" external create : - dictionary:[> `Document] GdomeT.t -> - mml: [> `Document] GdomeT.t -> - tex: [> `Document] GdomeT.t -> + dictionary_uri: string -> + mml_uri: string -> + tex_uri: string -> log:(int -> string -> unit) -> t = "ml_mathml_editor_new" diff --git a/helm/DEVEL/mathml_editor/ocaml/mathml_editor.ml b/helm/DEVEL/mathml_editor/ocaml/mathml_editor.ml index 472760184..04adc9450 100644 --- a/helm/DEVEL/mathml_editor/ocaml/mathml_editor.ml +++ b/helm/DEVEL/mathml_editor/ocaml/mathml_editor.ml @@ -32,8 +32,8 @@ let default_mathml_stylesheet_path = I_mathml_editor.get_default_mathml_styleshe let default_tex_stylesheet_path = I_mathml_editor.get_default_tex_stylesheet_path () ;; -let create ~dictionary ~mml ~tml ~log = - I_mathml_editor.create dictionary#as_Document mml#as_Document tml#as_Document log +let create ~dictionary_uri ~mml_uri ~tml_uri ~log = + I_mathml_editor.create dictionary_uri mml_uri tml_uri log ;; let freeze = I_mathml_editor.freeze diff --git a/helm/DEVEL/mathml_editor/ocaml/mathml_editor.mli b/helm/DEVEL/mathml_editor/ocaml/mathml_editor.mli index f215561f5..f294fcfdd 100644 --- a/helm/DEVEL/mathml_editor/ocaml/mathml_editor.mli +++ b/helm/DEVEL/mathml_editor/ocaml/mathml_editor.mli @@ -28,9 +28,9 @@ val default_mathml_stylesheet_path : string val default_tex_stylesheet_path : string val create : - dictionary:< as_Document : [> `Document] GdomeT.t; .. > -> - mml:< as_Document : [> `Document] GdomeT.t; .. > -> - tml:< as_Document : [> `Document] GdomeT.t; .. > -> + dictionary_uri: string -> + mml_uri: string -> + tml_uri: string -> log:(int -> string -> unit) -> I_mathml_editor.t val freeze : editor:I_mathml_editor.t -> bool diff --git a/helm/DEVEL/mathml_editor/ocaml/ml_mathml_editor.c b/helm/DEVEL/mathml_editor/ocaml/ml_mathml_editor.c index 4f84fffe3..e4cda57e1 100644 --- a/helm/DEVEL/mathml_editor/ocaml/ml_mathml_editor.c +++ b/helm/DEVEL/mathml_editor/ocaml/ml_mathml_editor.c @@ -88,9 +88,9 @@ ml_mathml_editor_get_default_tex_stylesheet_path(value unit) } value -ml_mathml_editor_new(value dictionary, - value tml_mml, - value tml_tex, +ml_mathml_editor_new(value dictionary_uri, + value tml_mml_uri, + value tml_tex_uri, value log_message_cb) { static struct custom_operations ops = @@ -106,9 +106,9 @@ ml_mathml_editor_new(value dictionary, value v = alloc_custom(&ops, sizeof(ml_Editor*), 0, 1); ml_Editor** ml_editor_ref = (ml_Editor**) Data_custom_val(v); ml_Editor* ml_editor = *ml_editor_ref = malloc(sizeof(ml_Editor)); - ml_editor->c_editor = c_mathml_editor_new(Document_val(dictionary), - Document_val(tml_mml), - Document_val(tml_tex), + ml_editor->c_editor = c_mathml_editor_new(String_val(dictionary_uri), + String_val(tml_mml_uri), + String_val(tml_tex_uri), ml_mathml_editor_log_callback, (void*) ml_editor); ml_editor->callback = log_message_cb; diff --git a/helm/DEVEL/mathml_editor/test/editor.cc b/helm/DEVEL/mathml_editor/test/editor.cc index 398d3133d..eab57f709 100644 --- a/helm/DEVEL/mathml_editor/test/editor.cc +++ b/helm/DEVEL/mathml_editor/test/editor.cc @@ -152,7 +152,7 @@ main(int argc, char* argv[]) TDictionary dictionary(logger); logger.info("loading the dictionary..."); - dictionary.load("./dictionary-test.xml"); + dictionary.load("/usr/share/editex/dictionary-tex.xml"); logger.info("loading the stylesheet..."); DOM::DOMImplementation di;