diff options
| author | hallgren <hallgren@chalmers.se> | 2011-02-28 12:41:05 +0000 |
|---|---|---|
| committer | hallgren <hallgren@chalmers.se> | 2011-02-28 12:41:05 +0000 |
| commit | a9287e83af1b6b87b216331fe62218d46079ce9f (patch) | |
| tree | c47dcd226562c52e4d8f6c043724b3fd227ad1d6 /src/editor | |
| parent | 0dfbc9b73049ad810d04314b95729511863c3b51 (diff) | |
gfse: minor documentation and style improvements
Diffstat (limited to 'src/editor')
| -rw-r--r-- | src/editor/simple/about.html | 4 | ||||
| -rw-r--r-- | src/editor/simple/editor.css | 2 |
2 files changed, 5 insertions, 1 deletions
diff --git a/src/editor/simple/about.html b/src/editor/simple/about.html index 2bcf686b5..6905dae10 100644 --- a/src/editor/simple/about.html +++ b/src/editor/simple/about.html @@ -94,6 +94,7 @@ Available editing operations: occurences of it in function types will be updated accordingly. <li>Functions can be added, removed and edited. Concrete syntaxes are updated to reflect changes. + <li>Functions can be reordered using drag-and-drop. </ul> Error checks: @@ -123,6 +124,7 @@ Available editing operations: be edited. <li>Parameter types can be added, removed and edited. <li>Operation definitons can be added, removed and edited. + <li>Definitions can be reordered (using drag-and-drop) </ul> Error checks: @@ -157,7 +159,7 @@ to be accessed from multiple devices. <hr> <div class=modtime><small> -<!-- hhmts start --> Last modified: Fri Feb 18 15:50:10 CET 2011 <!-- hhmts end --> +<!-- hhmts start --> Last modified: Wed Feb 23 17:37:16 CET 2011 <!-- hhmts end --> </small></div> <address> <a href="http://www.cse.chalmers.se/~hallgren/">TH</a> diff --git a/src/editor/simple/editor.css b/src/editor/simple/editor.css index 2c09897a0..56cfd5adb 100644 --- a/src/editor/simple/editor.css +++ b/src/editor/simple/editor.css @@ -27,6 +27,8 @@ td.right { text-align: right; } div.indent { padding-left: 1em; min-width: 1em; min-height: 1em; } +div.fun, div.param, div.lincat, div.oper, div.lin +{ padding-left: 2em; text-indent: -2em; } .more, .delete { font-weight: bold; font-family: sans-serif; } .more, .delete, .edit { cursor: pointer; } |
