Guide du Terminal⚓︎
Exemple⚓︎
Technique⚓︎
Techniquement, le terminal est obtenu en utilisant le plugin Terminal de jQuery1.
On crée un <div> qui possède un identificateur numéro (entier commençant à 1 et auto-incrémenté). Ce <div> est ensuite colorié à l'aide du plugin Terminal.
Technique
Un problème provient du focus du terminal. Par défaut, le dernier terminal créé aura le focus, ce qui souvent nous emmène en bas de page...
La solution a été de créer deux <div>:
- Le premier
<div>est un simple bloc de texte mimant un Terminal. Il est appelé fake_id. - Le second
<div>contient effectivement le Terminal. Il ne se créera que si l'événement onclick du<div id = fake_id>est déclenché.
Vraiment très technique
Voir aussi les fonctions pyterm et start_term de interpreter.js.
-
C'est pour cela qu'on ne peut pas se passer de jQuery actuellement. ↩