diff options
| author | hallgren <hallgren@chalmers.se> | 2011-08-08 17:28:24 +0000 |
|---|---|---|
| committer | hallgren <hallgren@chalmers.se> | 2011-08-08 17:28:24 +0000 |
| commit | d4638f54bad7523907ebb6502af48470351d8f9e (patch) | |
| tree | 81cbdcb6a951e18eb8f39f62c6b06419595234c3 /src/runtime/javascript/minibar/minibar.html | |
| parent | e50731c5111cc4a4addbdb157de2d73001976c2d (diff) | |
minibar: refactoring for improved modularity
Two smaller objects have been factored out from the Minibar object:
Input and Translations. These have been placed in two separate files:
minibar_input.js and minibar_translations.js. Some common auxiliary functions
have also been moved to a separate file: minibar_support.js
Diffstat (limited to 'src/runtime/javascript/minibar/minibar.html')
| -rw-r--r-- | src/runtime/javascript/minibar/minibar.html | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/runtime/javascript/minibar/minibar.html b/src/runtime/javascript/minibar/minibar.html index a6bc8f085..086b8fad6 100644 --- a/src/runtime/javascript/minibar/minibar.html +++ b/src/runtime/javascript/minibar/minibar.html @@ -23,7 +23,7 @@ & <a href="http://www.grammaticalframework.org:41296/translate/">Translator</a>] </small> <small class=modtime> -HTML <!-- hhmts start --> Last modified: Wed Aug 3 15:09:58 CEST 2011 <!-- hhmts end --> +HTML <!-- hhmts start --> Last modified: Mon Aug 8 18:04:22 CEST 2011 <!-- hhmts end --> </small> <address> <a href="http://www.cse.chalmers.se/~hallgren/">TH</a> @@ -31,6 +31,9 @@ HTML <!-- hhmts start --> Last modified: Wed Aug 3 15:09:58 CEST 2011 <!-- hhmt <script type="text/JavaScript" src="support.js"></script> <script type="text/JavaScript" src="minibar.js"></script> +<script type="text/JavaScript" src="minibar_input.js"></script> +<script type="text/JavaScript" src="minibar_translations.js"></script> +<script type="text/JavaScript" src="minibar_support.js"></script> <script type="text/JavaScript" src="pgf_online.js"></script> <script type="text/javascript" src="minibar_online.js"></script> |