* php scripts in export html code in org-mode
@ 2021-12-21 14:45 Joseph Vidal-Rosset
2021-12-22 14:26 ` Ihor Radchenko
0 siblings, 1 reply; 3+ messages in thread
From: Joseph Vidal-Rosset @ 2021-12-21 14:45 UTC (permalink / raw)
To: org-mode-email
Hello,
Here is my problem. The code below, that is the code of the page called
"index.php" works.
< https://www.vidal-rosset.net/fCube/ >
But I would be happy to have this prover in this web page
<
https://www.vidal-rosset.net/fcube_an_efficient_prover_for_intuitionistic_propositional_logic.html
>
that I have made from org-mode.
Unfortunately, all my efforts to integrate this code to export failed,
and finally I get a JSON.parse error, (
json-parse-unexpected-character-at-line-1-column-1-of-the-json-data )
that I suspect to be a PHP error code.
Your help is welcome.
Best wishes, and Merry Christmas !
Jo.
PS: the code to export from an org-mode file would be this one (that of
index.php file, presently):
<?php
if ($f_encoded = ($_POST['formula'] ?? null)) {
$formula = urldecode($f_encoded);
// swipl will need the full path, so
// assume quineweb.pl is in the same folder as this php script
$fcube = __DIR__ . '/fcubeweb.pl';
$descp = [
0 => ['pipe','r'],
1 => ['pipe','w'],
//2 => null
];
$proc = proc_open("swipl -g fcube -g halt $fcube", $descp, $pipes);
if (is_resource($proc)) {
fwrite($pipes[0], $formula);
fclose($pipes[0]);
$Proof = stream_get_contents($pipes[1]);
fclose($pipes[1]);
$return_value = proc_close($proc);
header('Content-type: application/json');
echo json_encode(['proof'=>$Proof,'formula'=>'TBD']);
}
exit;
}
?>
<!DOCTYPE html>
<html lang="en">
<head>
<!-- 2020-08-13 jeu. 09:08 -->
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>index</title>
<meta name="generator" content="Org mode">
<link rel="stylesheet" type="text/css" href="css/org.css"/>
<link rel="stylesheet" type="text/csl" href="ieee.csl"/>
<link rel="icon" href="ico/favicon.ico" type="image/x- icon">
<script type="text/javascript">
/*
@licstart The following is the entire license notice for the
JavaScript code in this tag.
Copyright (C) 2012-2020 Free Software Foundation, Inc.
The JavaScript code in this tag is free software: you can
redistribute it and/or modify it under the terms of the GNU
General Public License (GNU GPL) as published by the Free Software
Foundation, either version 3 of the License, or (at your option)
any later version. The code is distributed WITHOUT ANY WARRANTY;
without even the implied warranty of MERCHANTABILITY or FITNESS
FOR A PARTICULAR PURPOSE. See the GNU GPL for more details.
As additional permission under GNU GPL version 3 section 7, you
may distribute non-source (e.g., minimized or compacted) forms of
that code without the copy of the GNU GPL normally required by
section 4, provided you include this license notice and a URL
through which recipients can access the Corresponding Source.
@licend The above is the entire license notice
for the JavaScript code in this tag.
*/
<!--/*--><![CDATA[/*><!--*/
function CodeHighlightOn(elem, id)
{
var target = document.getElementById(id);
if(null != target) {
elem.cacheClassElem = elem.className;
elem.cacheClassTarget = target.className;
target.className = "code-highlighted";
elem.className = "code-highlighted";
}
}
function CodeHighlightOff(elem, id)
{
var target = document.getElementById(id);
if(elem.cacheClassElem)
elem.className = elem.cacheClassElem;
if(elem.cacheClassTarget)
target.className = elem.cacheClassTarget;
}
/*]]>*///-->
</script>
</head>
<body>
<div id="content">
<div class="head">
<div class="title">
<p>
<a href= "https://www.swi-prolog.org/"><img src="swi-prolog-logo.png"
width="50" height="50"></a>
<a href="index.html">FCUBE 4.1 WITH INFIX NOTATION</a>
</p>
</div>
</nav>
<div>
<div>
</script>
<script>
MathJax = {
loader: {
load: ['[tex]/bussproofs']
},
tex: {
packages: {'[+]': ['bussproofs']},
tags: 'ams'
}
};
</script>
<script id="MathJax-script " async
src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js">
</script>
</head>
<body>
<div id="content">
<h3>Syntax for input formulas: ~a , a & b, a | b ,a =>b , a <=> b
(for, respectively, negation, conjunction, disjunction, conditional and
biconditional . </h3>
<label>
<p> Choose a formula in the list below, or input your one</p>
<?=formulae_predef()?>
</label>
</div>
<textarea id=formula rows=1 cols=100% title='enter your formula
here, or select one predefined above'>
</textarea>
<div>
<button id=decide_formula><img src="swi-prolog-logo.png"
width="35" height="35"> <b> ? - </b></button>
<pre id=proof_show>Either an intuitionistic proof or an
intuitionistic refutation will show here</pre>
</div>
</div>
<?=css()?>
<?=js()?>
</html>
<?php
function formulae_predef() {
ob_start();?>
<select id=formulae_predef>
<option> ~ a | a /* Excluded Middle */ </option>
<option> ~ ~ a => a /* Double Negation Elimination */ </option>
<option>((a => b) => a) => a /* Pierce Formula */ </option>
<option>((~ a => b) & (a => b)) => b /* Dilemma */ </option>
<option>(a => b) | (b => a) /* Dummett Formula */ </option>
<option>~(a & b) => (~ a | ~ b) /* Classical de Morgan Implication
*/</option>
<option>(~ a | ~ b) => ~(a & b) /* Intuitionistic de Morgan
Implication */</option>
<option>~(a | b) <=> (~ a & ~ b) /* Intuitionistic De Morgan
Equivalence */</option>
<option>(~ a => a) <=> ~ ~ a /* Intuitionistic Equivalence */</option>
<option> ( ( p
| ( q
& r ) )
<=> ( ( p
| q )
& ( p
| r ) ) ) /* Pelletier Problem 13 SYN045+1 */</option>
<option> ( ( ( p
& ( q
=> r ) )
=> s )
<=> ( ( ~ p
| q
| s )
& ( ~ p
| ~ r
| s ) ) ) /* Pelletier Problem 17 SYN047+1 */ </option>
<option>((a | b) => c) <=> ((a => c) & (b => b)) </option>
<option>((a & b) => c) <=> ((a => c) | (b => c)) </option>
<!-- add more, to illustrate accepted syntax -->
</select>
<?php return ob_get_clean();
}
function css() {
ob_start();?>
<style>
</style>
<?php return ob_get_clean();
}
function js() {
ob_start();?>
<script>
window.onload = () => {
const request = (url,formula) => fetch(url,{
method: 'POST',
headers: { 'Content-Type':
'application/x-www-form-urlencoded;charset=UTF-8' },
body: 'formula='+encodeURIComponent(formula)
}).then(r => r.json())
decide_formula.onclick = async (ev) => {
let f = formula.value.trim()
if (!f.endsWith('.')) f += '.'
try {
let result = await request("<?=$_SERVER['REQUEST_URI']?>", f)
if (result.proof)
proof_show.textContent = result.proof
else
proof_show.innerHTML = 'there was a
problem:<b>'+JSON.stringify(result)+'<b>'
} catch(e) {
alert(e.message)
}
}
formulae_predef.onchange = (ev) => {
formula.value = ev.target.value
}
}
</script><?php
return ob_get_clean();
}
^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2021-12-22 19:04 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2021-12-21 14:45 php scripts in export html code in org-mode Joseph Vidal-Rosset
2021-12-22 14:26 ` Ihor Radchenko
2021-12-22 18:54 ` Re : " Joseph Vidal-Rosset
Code repositories for project(s) associated with this public inbox
https://git.savannah.gnu.org/cgit/emacs/org-mode.git
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).