Une AbstractWindow défini une fenêtre CtCoq minimale, composée, d'une fenêtre de script, d'un menu, d'une barre d'outils, d'une fenêtre de buts et d'une fenêtre de théorèmes. Toutes les fenêtres de Pcoq sont des sous-classes de AbstractWindow, à savoir MainWindow, ProofWindow et ProofTextWindow.
Fenêtre principale de Pcoq. C'est la première fenêtre qui
apparait quand on lance l'application. C'est une sous-classe de
AbstractWindow.
Fenêtre de preuve additionnelle. Une ProofWindow peut être créée à partir d'une MainWindow ou d'une ProofWindow.
La destruction d'une ProofWindow entraine la destruction de toutes les ProofWindow créées à partir de celle-ci (?) => fenêtres filles.
Fenêtre "dégénérée", ne contenant que la fenêtre de script et le menu.
Abstract class pour les évènements générés lorsqu'une requête au parser a été effectuée.
Abstract class pour les évènements générés lorsqu'une requête au proover a été effectuée.
Une connection à un process (parser ou proover) distant (ou non). Les sous-classes de cette classe abstraite implémentent des méthodes spécifiques au requêtes acceptées par le process distant, ainsi qu'une méthode pour llire et interprèter les retours.
Représente une connection au proover.
Représente une connection au parser.
Une classe abstraite qui permet d'executer des tâches dans un
thread séparé. (cf.
http://java.sun.com/products/jfc/swingdoc/threads.html)
Afin de respecter la règle lorsqu'on utilise Swing, qui veut
que toutes les modification sur un composant s'effectue dans
le thread de dispatch des évènements, on utilise un thread
séparé par éffectuer les requêtes au parser et au proover,
mais toutes les mises à jour graphiques sont faites dans le
event dispatching thread.
On "sérialise" l'accès au proover en synchronisant l'accès à
l'objet proover.
Lorsque le thread a terminé sa requête, il poste un evt a
destination de la fenêtre qui l'a initiée.
Le résultat produit par le thread est inclu dans
SwingWorker. L'évènement posté
Une sous classe de SwingWorker, qui envoi une requête au parser et attend la réponse, pour pouvoir poster un ParsedEvent à destination de la "Window" qui à demander d'executer cette requete.
Idem que ParseRequestWorker, mais envoit une requête au proover.