From 2c9f4fddc259b09b6e71b18eef78f0bed38eeb14 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 31 Jan 2020 21:12:57 +0100 Subject: [PATCH] =?utf8?q?update=20in=20binaries=20for=20=CE=BB=CE=B4?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit roles: initial infrastructure for the web interface --- .../contribs/lambdadelta/bin/roles/roles.ml | 7 ++- .../lambdadelta/bin/roles/rolesGlobal.ml | 5 ++ .../lambdadelta/bin/roles/rolesGlobal.mli | 2 + .../lambdadelta/bin/roles/webEngine.ml | 58 +++++++++++++++++++ .../lambdadelta/bin/roles/webEngine.mli | 12 ++++ 5 files changed, 83 insertions(+), 1 deletion(-) create mode 100644 matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/roles/webEngine.mli diff --git a/matita/matita/contribs/lambdadelta/bin/roles/roles.ml b/matita/matita/contribs/lambdadelta/bin/roles/roles.ml index bbabd2264..c3dce2b8d 100644 --- a/matita/matita/contribs/lambdadelta/bin/roles/roles.ml +++ b/matita/matita/contribs/lambdadelta/bin/roles/roles.ml @@ -13,9 +13,12 @@ module EE = RolesEngine module EG = RolesGlobal module ET = RolesTypes module EU = RolesUtils +module WE = WebEngine +let help_B = " Set this base url (default: http://helm.cs.unibo.it/lambdadelta/)" let help_C = " Set this working directory (default: current directory)" let help_L = " Debug osn lexer" +let help_W = " Run as an LWS application" let help_X = " Reset all options to defaults" let help_a = " Add selected names to a role" let help_m = " Add roles relating matching names" @@ -25,7 +28,7 @@ let help_r = " Load current status" let help_s = " Start a stage with this version" let help_t = " Toggle the selection of this pointed entry" let help_w = " Save current status" -let help = "Usage: roles [ -LXamprw | -C | -os | -t | ]*" +let help = "Usage: roles [ -LWXamprw | -B | -C | -os | -t | ]*" let add_tops s = EE.add_tops (EU.version_of_string s) @@ -43,8 +46,10 @@ let process s = let _main = try Arg.parse [ + "-B", Arg.String ((:=) EG.base_url), help_B; "-C", Arg.String ((:=) EG.wd), help_C; "-L", Arg.Set EG.debug_lexer, help_L; + "-W", Arg.Unit WE.init, help_W; "-X", Arg.Unit EG.clear, help_X; "-a", Arg.Unit EE.add_role, help_a; "-m", Arg.Unit EE.add_matching, help_m; diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesGlobal.ml b/matita/matita/contribs/lambdadelta/bin/roles/rolesGlobal.ml index 8a2679b6d..6a4c37369 100644 --- a/matita/matita/contribs/lambdadelta/bin/roles/rolesGlobal.ml +++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesGlobal.ml @@ -9,14 +9,19 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +let default_base_url = "http://helm.cs.unibo.it/lambdadelta/" + let default_wd = "" let default_debug_lexer = false +let base_url = ref default_base_url + let wd = ref default_wd let debug_lexer = ref default_debug_lexer let clear () = + base_url := default_base_url; wd := default_wd; debug_lexer := default_debug_lexer diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesGlobal.mli b/matita/matita/contribs/lambdadelta/bin/roles/rolesGlobal.mli index 980160a6e..87b052089 100644 --- a/matita/matita/contribs/lambdadelta/bin/roles/rolesGlobal.mli +++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesGlobal.mli @@ -9,6 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +val base_url: string ref + val wd: string ref val debug_lexer: bool ref diff --git a/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml new file mode 100644 index 000000000..7fc942960 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml @@ -0,0 +1,58 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module KP = Printf + +module EG = RolesGlobal +module EE = RolesEngine + +let open_out_html author description title css icon = +(* + YW.open_out "application/xhtml+xml" 0; +*) + KP.printf "\n"; + KP.printf "\n"; + KP.printf "\n"; + KP.printf "\n"; + KP.printf " \n"; + KP.printf " \n"; + KP.printf " \n"; + KP.printf " \n"; + KP.printf " \n"; + KP.printf " \n"; + KP.printf " \n" author; + KP.printf " \n" description; + KP.printf " %s" title; + KP.printf " \n" css; + KP.printf " \n" icon; + KP.printf "\n"; + KP.printf "\n" + +let close_out_html () = + KP.printf "\n"; + KP.printf "\n" +(* + YW.close_out () +*) +let open_out () = + let author = "λδ development binary: roles manager" in + let description = "λδ development binary: roles manager" in + let title = "Roles Manager" in + let css = Filename.concat !EG.base_url "css/roles.css" in + let icon = Filename.concat !EG.base_url "images/crux_32.ico" in + open_out_html author description title css icon + +let close_out () = + close_out_html () + +let init () = + open_out (); + close_out () diff --git a/matita/matita/contribs/lambdadelta/bin/roles/webEngine.mli b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.mli new file mode 100644 index 000000000..8540afa8e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.mli @@ -0,0 +1,12 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +val init: unit -> unit -- 2.39.2