Commit Graph

164 Commits

Author SHA1 Message Date
hallgren
4f7255dae2 minibar: restructured code and improved user interface
* Keyboard input and completion should now work much more smoothly:
  + When you press space, the current word will be completed (if incomplete)
    and a new magnet will be created. If there is more than one possible
    completion, no magnet is created, but the common prefix of the possible
    completions is added to the text box.
  + Instead of asking the server for possible completions every time a new
    letter is added to the curent word, minibar only ask for completions for
    whole words and then filters the list locally when more letters are entered,
    speeding things up when server responses are slow.

* Code restructuring:
  + The PGF server API has been moved to its own file: pgf_online.js. This
    allows it to be reused in other applicaitons without importing the entire
    minibar. It also allows minibar to be used with different server interfaces.
  + The minibar code has been rewritten to avoid storing state information
    in the document tree and accessing it by referring to named document
    elements. The code now also avoids using string literals contaning
    the names of top-level functions to specify event handlers for buttons
    and menus. (The code is no longer introspective, so alpha conversion will
    not change its meaning.)
2010-10-26 12:42:33 +00:00
hallgren
41edd0a84f support.js: some enhancements and new functions
+ ajax_http_get(url,callback) now checks the HTTP response status and shows an
  error message if the status is not OK (is not 200)
+ New function node(tag,attrs,children) to create document nodes with arbitraty
  attributes and children. The functions node() and text() should now be enough
  to construct arbitrary document trees in an easy, functional way, and many of
  the more specialized functions could be removed.
+ When calling the function button(label,action,key), the action can be a
  function instead of a string, so you can use local/anonymous functions.
+ New function debug(str) adds text to the element with id=debug, if it
  exists.
2010-10-26 11:52:04 +00:00
krasimir
9802d534c0 when faced with hard unification problem the type checker should just postpone the decision instead of failing immediately. added test case as well 2010-10-25 15:47:33 +00:00
krasimir
75e8cba592 when we print the bracketed string it is useful to print the attached metavariables as well 2010-10-25 12:21:12 +00:00
krasimir
8c751d404f change the TcM monad to continuation passing style. The old monad caused stack overflow for large search spaces 2010-10-21 15:01:52 +00:00
krasimir
09dde495ce support for proof search with high-order functions 2010-10-21 12:47:26 +00:00
krasimir
43cbc6693d bugfix in the term generation 2010-10-20 13:36:39 +00:00
krasimir
6e23da41a2 fixed typo which broke the parsing with -openclass 2010-10-20 09:04:48 +00:00
krasimir
5acec7be21 in the type checker monad we should use lazy pattern matching because otherwise we force the exhaustive tree generation to be strict 2010-10-19 13:04:41 +00:00
krasimir
51452d4ef0 added explicit depth parameter to the parsing API and the corresponding command in the shell 2010-10-18 16:51:25 +00:00
krasimir
afce46b386 typo in PGF.TypeCheck which spoiled the previous patch 2010-10-18 16:50:55 +00:00
krasimir
7fb5fddbb8 now we use the GF reasoner to fillin meta variables in the abstract trees generated from the parser 2010-10-18 15:55:14 +00:00
hallgren
0d1c3dc62b minibar.html: add a <noscript> element with a note that the page doesn't work unless JavaScript is enabled 2010-10-23 14:56:10 +00:00
hallgren
dd7cd640ea minibar.js: show the type error messages that can occur for grammars with dependent types 2010-10-18 12:15:30 +00:00
hallgren
5400728ef7 minibar.js: add an option to enable/disable the Random button 2010-10-17 16:48:21 +00:00
krasimir
9fdc7134e8 now since the type checking monad TcM is nondeterministic we can use the same monad in PGF.Forest.getAbsTrees 2010-10-14 14:28:40 +00:00
krasimir
cc2232e289 bugfix in PGF.VisualizeTree for handling trees with implicit arguments 2010-10-13 13:32:48 +00:00
krasimir
f4603cf9d4 fix PGF.Generate.restart. The restart should be done only if there are some solutions found 2010-10-13 12:38:51 +00:00
krasimir
95733f0b1b the exhaustive/random generator now knows how to handle computable functions in the types 2010-10-11 17:18:28 +00:00
krasimir
e7f6239bc6 now the generation from template with meta-variables respects the dependent types 2010-10-11 09:59:57 +00:00
krasimir
7d9bbea985 backtracking for random generation is not enough. we must restart the search after each solution 2010-10-02 13:34:58 +00:00
krasimir
be9ad26aea refactor the API for random generation again. Now PGF contains probabilities in the abstract syntax 2010-10-02 13:03:57 +00:00
hallgren
518a27a009 minibar: work on adding back support for typing multiple words without pressing enter in between
It mostly works now, but some minor issues still need to be fixed.
2010-09-29 13:03:40 +00:00
hallgren
31d0e84617 minibar: update about.html with description of recent changes 2010-09-28 11:46:32 +00:00
hallgren
6f2a3849f3 minibar/about.html: fix typos and formatting 2010-09-24 12:57:16 +00:00
hallgren
3d2bf753d4 minibar.html: specify charset, move initialization
Added a meta tag to specify that the file is in UTF-8. This makes the browser
(at least Firefox) assume that the JavaScript files are also in UTF-8, it seems.

Moved the call to start_minibar() from the <body onload="..."> to the end of
the file. The onload action is not executed until all images in the document
has been loaded, while javascipt at the end of the file is executed as soon
as the HTML file has been loaded. (Calling start_minibar() from the head of
the document would be too soon, since it refers to elements in the body,
which hasn't been loaded yet.)
2010-09-24 12:47:18 +00:00
krasimir
4e715c3952 the first revision of exhaustive and random generation with dependent types. Still not quite stable. 2010-09-22 15:49:16 +00:00
krasimir
bc92927692 cleanup and export the Probabilistic API from PGF 2010-09-22 09:06:19 +00:00
krasimir
efbc9e9d6d bugfix in PGF.Type.pType: Agda style types like {x : A} -> B should not be supported in GF 2010-09-12 12:26:38 +00:00
hallgren
c533314843 minibar.js: server API code cleanup 2010-09-14 17:15:37 +00:00
hallgren
ee36bac494 minibar.js: bug fix: the current word should be accepted when you press enter if it matches one of the possible completions exactly
The current word is also accepted if there is only one remaining possible
completion.
2010-09-14 16:48:20 +00:00
hallgren
ed9999784f minibar.js: add access keys to some of the buttons 2010-09-14 16:45:48 +00:00
hallgren
fa65026136 support.js: create buttons with access keys 2010-09-10 12:20:07 +00:00
hallgren
846b747cee minibar: default input language is now the user's preferred language, if possible
This is implemented using the userLanguage field in the grammar info output by
pgf-server.
2010-09-10 11:03:46 +00:00
hallgren
f5f8369d97 minibar: use AJAX instead of JSONP when possible
Using AJAX instead of JSONP can give better caching in the browser, since the
URL doesn't need to contain a (dynamically generated) callback function name.
But because of the same origin policy in JavaScript, AJAX can only be used when
the HTML file is served from the same server as the PGF. The new function
http_get_json in support.js uses AJAX if this is the case, and falls back to
JSONP otherwise.
2010-09-10 08:38:11 +00:00
hallgren
c662d116f6 Minibar: PGF server API: pass callback functions directly instead of passing function names as strings. 2010-09-05 18:06:45 +00:00
hallgren
b14592b0d3 minibar: fix broken link to brushed-metal background
Solution: include a local copy of brushed-metal.png
2010-09-05 18:01:44 +00:00
krasimir
b0e78f33bc PGF.Expr.normalForm does variable renaming 2010-08-30 07:37:12 +00:00
hallgren
3a120aaf17 Adapt minibar.js to the current GF web service API
Quick fix. More work needed for correct behaviour when multiple words are
entered at once.
2010-08-27 16:46:14 +00:00
krasimir
9aa7c88c5a native representation for HOAS in PMCFG and incremental type checking of the parse forest 2010-08-09 10:10:08 +00:00
krasimir
b20821dfc3 more advanced complete function in the PGFService 2010-08-24 15:58:22 +00:00
krasimir
71ea541765 two new functions in the PGF API: mkAbs, unAbs 2010-07-31 16:40:16 +00:00
krasimir
b227c8a586 now the meta id of the meta variables is accessible via the PGF API 2010-07-31 12:52:20 +00:00
krasimir
ebe5b87738 added function unType in PGF 2010-07-31 12:47:10 +00:00
krasimir
df555d54fb fix the algorithm for items cutting in the partial parser 2010-07-15 14:01:51 +00:00
krasimir
ef68e209c2 fix the loopchecking in PGF.Forest.bracketedTokn 2010-07-13 12:04:06 +00:00
hallgren
c9cca8a77e Add missing <td> tags in the HTML constructed by functio show_groupedtranslations 2010-07-13 11:54:42 +00:00
hallgren
032cd65f8f Bug fix in minibar.js: no translations where shown when using option show_grouped_translations: false
This affected minibar.html but not phrasebook.html and was
caused by accidental shadowing of function tr in function show_translations.
2010-07-13 11:35:28 +00:00
hallgren
866ef5ead0 Make minibar.js work again after backwards incompatible changes to the data structures output by pgf-server.
The canParse field was removed without notice.
2010-07-13 10:22:03 +00:00
krasimir
5ea08bd2e8 bugfix in the decoding of literals in PGF.Binary 2010-07-13 08:24:03 +00:00