Ich habe eine Web-IDE (WIDE) für den Beweis in der Informatik erstellt. Sie wissen vielleicht, dass es drei der häufigsten Beweisassistenten gibt, die Athena, Isabelle und Coq heißen. Die meisten Informatiker vergessen möglicherweise ihre Syntax, Gültigkeitsbereiche usw. Meine Web-IDE arbeitet mit Drag-and-Drop-Designs und Beispielen. Sie können zusätzlichen Code bearbeiten und darauf schreiben, Sie können ihn herunterladen, Sie können ihn freigeben, Sie können ihn speichern usw. Es hat auch einen eigenen Parser. Soweit ist alles in Ordnung. Achtung! Hier ist meine Frage: Wie kann ich die Benutzercodes ausführen und das Ergebnis erhalten (speziell für Athenahttp: //proofcentral.org) wenn Benutzer ihren Code auf meiner Web-IDE ausführen möchten. Eigentlich kann ich das über mouse_event (user32) und andere mit pinvoke (platform invoke) machen. Mein Programm sendet die Codes über das Web an den laufenden PC (nicht an den Server. Da der Server keinen Bildschirm hat und das Programm nicht weiß, wohin sie klicken), erhält der PC die Codes. Dann klickt das Programm auf das "Emacs" -Symbol. Nach ein paar Sekunden (zum Öffnen und Hochladen von DLLs von Athena) fügt das Programm den Code von Athena in die Emacs-Shell ein. Emacs führen diesen Code aus und geben das Ergebnis zurück. Danach wählt das Programm das Ergebnis aus, kopiert es und sendet es an Web IDE zurück. Dies ist jedoch ein verrückter und kniffliger Weg. Ich würde gerne den besten Weg machen. Danke für Ihre Aufmerksamkeit. Best