From: Stefano Zacchiroli Date: Sat, 24 Jan 2004 12:35:09 +0000 (+0000) Subject: .in version of "configuration" modules X-Git-Tag: V_0_2_3~147 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1bd503d31db62ec1f4b1dfb416c11615f3af7248;p=helm.git .in version of "configuration" modules --- diff --git a/helm/gTopLevel/chosenTermEditor.ml b/helm/gTopLevel/chosenTermEditor.ml deleted file mode 100644 index 25dcfd2e5..000000000 --- a/helm/gTopLevel/chosenTermEditor.ml +++ /dev/null @@ -1,4 +0,0 @@ -include TermEditor -(* -include TexTermEditor -*) diff --git a/helm/gTopLevel/chosenTermEditor.ml.in b/helm/gTopLevel/chosenTermEditor.ml.in new file mode 100644 index 000000000..d501e8d06 --- /dev/null +++ b/helm/gTopLevel/chosenTermEditor.ml.in @@ -0,0 +1 @@ +@CHOSEN_TERM_EDITOR@ diff --git a/helm/gTopLevel/chosenTransformer.ml b/helm/gTopLevel/chosenTransformer.ml deleted file mode 100644 index 85e27049a..000000000 --- a/helm/gTopLevel/chosenTransformer.ml +++ /dev/null @@ -1,2 +0,0 @@ -(* include ApplyStylesheets *) -include ApplyTransformation diff --git a/helm/gTopLevel/chosenTransformer.ml.in b/helm/gTopLevel/chosenTransformer.ml.in new file mode 100644 index 000000000..e81993ec3 --- /dev/null +++ b/helm/gTopLevel/chosenTransformer.ml.in @@ -0,0 +1 @@ +@CHOSEN_TRANSFORMER@ diff --git a/helm/gTopLevel/disambiguatingParser.ml b/helm/gTopLevel/disambiguatingParser.ml deleted file mode 100644 index eb89b1170..000000000 --- a/helm/gTopLevel/disambiguatingParser.ml +++ /dev/null @@ -1,105 +0,0 @@ -(* Copyright (C) 2004, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -exception NoWellTypedInterpretation - -module AndreaAndZackDisambiguatingParser = - struct - module EnvironmentP3 = DisambiguateTypes.EnvironmentP3 - - module Make (C : DisambiguateTypes.Callbacks) = - struct - let - disambiguate_term mqi_handle context metasenv term_as_string environment - = - let module Disambiguate' = Disambiguate.Make (C) in - let term = - CicTextualParser2.parse_term (Stream.of_string term_as_string) - in - Disambiguate'.disambiguate_term - mqi_handle context metasenv term environment - end - end - - -module CSCTextualDisambiguatingParser = - struct - module EnvironmentP3 = OldDisambiguate.EnvironmentP3 - - module Make (C : DisambiguateTypes.Callbacks) = - struct - let - disambiguate_term mqi_handle context metasenv term_as_string environment - = - let module Disambiguate' = OldDisambiguate.Make (C) in - let name_context = - List.map - (function - Some (n,_) -> Some n - | None -> None - ) context - in - let lexbuf = Lexing.from_string term_as_string in - let dom,mk_metasenv_and_expr = - CicTextualParserContext.main - ~context:name_context ~metasenv CicTextualLexer.token lexbuf - in - Disambiguate'.disambiguate_input mqi_handle - context metasenv dom mk_metasenv_and_expr environment - end - end - -module CSCTexDisambiguatingParser = - struct - module EnvironmentP3 = OldDisambiguate.EnvironmentP3 - - module Make (C : DisambiguateTypes.Callbacks) = - struct - let - disambiguate_term mqi_handle context metasenv term_as_string environment - = - let module Disambiguate' = OldDisambiguate.Make (C) in - let name_context = - List.map - (function - Some (n,_) -> Some n - | None -> None - ) context - in - let lexbuf = Lexing.from_string term_as_string in - let dom,mk_metasenv_and_expr = - TexCicTextualParserContext.main - ~context:name_context ~metasenv TexCicTextualLexer.token lexbuf - in - Disambiguate'.disambiguate_input mqi_handle - context metasenv dom mk_metasenv_and_expr environment - end - end - -include AndreaAndZackDisambiguatingParser -(* -include CSCTextualDisambiguatingParser -include CSCTexDisambiguatingParser -*) diff --git a/helm/gTopLevel/disambiguatingParser.ml.in b/helm/gTopLevel/disambiguatingParser.ml.in new file mode 100644 index 000000000..25953b502 --- /dev/null +++ b/helm/gTopLevel/disambiguatingParser.ml.in @@ -0,0 +1,102 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +exception NoWellTypedInterpretation + +module AndreaAndZackDisambiguatingParser = + struct + module EnvironmentP3 = DisambiguateTypes.EnvironmentP3 + + module Make (C : DisambiguateTypes.Callbacks) = + struct + let + disambiguate_term mqi_handle context metasenv term_as_string environment + = + let module Disambiguate' = Disambiguate.Make (C) in + let term = + CicTextualParser2.parse_term (Stream.of_string term_as_string) + in + Disambiguate'.disambiguate_term + mqi_handle context metasenv term environment + end + end + + +module CSCTextualDisambiguatingParser = + struct + module EnvironmentP3 = OldDisambiguate.EnvironmentP3 + + module Make (C : DisambiguateTypes.Callbacks) = + struct + let + disambiguate_term mqi_handle context metasenv term_as_string environment + = + let module Disambiguate' = OldDisambiguate.Make (C) in + let name_context = + List.map + (function + Some (n,_) -> Some n + | None -> None + ) context + in + let lexbuf = Lexing.from_string term_as_string in + let dom,mk_metasenv_and_expr = + CicTextualParserContext.main + ~context:name_context ~metasenv CicTextualLexer.token lexbuf + in + Disambiguate'.disambiguate_input mqi_handle + context metasenv dom mk_metasenv_and_expr environment + end + end + +module CSCTexDisambiguatingParser = + struct + module EnvironmentP3 = OldDisambiguate.EnvironmentP3 + + module Make (C : DisambiguateTypes.Callbacks) = + struct + let + disambiguate_term mqi_handle context metasenv term_as_string environment + = + let module Disambiguate' = OldDisambiguate.Make (C) in + let name_context = + List.map + (function + Some (n,_) -> Some n + | None -> None + ) context + in + let lexbuf = Lexing.from_string term_as_string in + let dom,mk_metasenv_and_expr = + TexCicTextualParserContext.main + ~context:name_context ~metasenv TexCicTextualLexer.token lexbuf + in + Disambiguate'.disambiguate_input mqi_handle + context metasenv dom mk_metasenv_and_expr environment + end + end + +@CHOSEN_TERM_PARSER@ +