hallgren 26da60d0a9 minibar.js: add an option to enable/disable the Random button

2010-10-17 16:48:21 +00:00

..

compiler

added option -depth to command gr

2010-10-12 13:36:37 +00:00

runtime

minibar.js: add an option to enable/disable the Random button

2010-10-17 16:48:21 +00:00

server

the PGF service now can do both random and exhaustive generation. these functions now return both the generated tree and its linearization

2010-10-13 12:32:49 +00:00

tools

GF emacs mode

2010-08-19 11:36:24 +00:00

ui

WebUI: show error when depth/limit has invalid value

2010-10-13 12:53:42 +00:00