2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
15 * MatitaWeb is a web interface for the Matita interactive theorem prover.
16 * Its user interface is composed of two main panes:
18 * -> the script area, whose content you are currently reading, which is
19 * used to input definitions and theorems to be checked by Matita;
20 * -> a top area with a title bar and a toolbar providing all the
21 * interactive operations apart from proof authoring.
23 * The toolbar on the top is divided in two sections:
24 * -> the large blue tiles provide the basic operations concerning the
25 * execution and checking of a proof script, including step-by-step
27 * -> the smaller circular buttons on the right provide script management
28 * operations (create, open, save...)
30 *
\ 5img class="topimg intext" src="icons/advance.png"
\ 6 Advance - executes the next step of the script
31 *
\ 5img class="topimg intext" src="icons/retract.png"
\ 6 Retract - undoes the execution of the last step of the script
32 *
\ 5img class="topimg intext" src="icons/top.png"
\ 6 Top - undoes the whole script, returning to the start
33 *
\ 5img class="topimg intext" src="icons/position.png"
\ 6 Play - executes the script until the current position of the cursor
34 *
\ 5img class="topimg intext" src="icons/bottom.png"
\ 6 Bottom - executes the whole script, until the end (or an error) is reached
36 *
\ 5img class="toolbarimg intext" src="icons/add.png"
\ 6 New script - creates a new empty script, opening a window to specify where
37 * the script should be placed in the library
38 *
\ 5img class="toolbarimg intext" src="icons/folder.png"
\ 6 Open script - opens an existing script in the library
39 *
\ 5img class="toolbarimg intext" src="icons/save.png"
\ 6 Save script - saves the current script
40 *
\ 5img class="toolbarimg intext" src="icons/saveas.png"
\ 6 Save script as - saves the current script with a new name
41 *
\ 5img class="toolbarimg intext" src="icons/upload.png"
\ 6 Import local script - allows the user to import a script from the local
42 * machine into the web interface buffer
43 *
\ 5img class="toolbarimg intext" src="icons/check.png"
\ 6 Commit - commits user changes to the shared library
44 *
\ 5img class="toolbarimg intext" src="icons/refresh.png"
\ 6 Update - synchronizes the user working copy by updating it with the
45 * changes in the shared library
46 *
\ 5img class="toolbarimg intext" src="icons/questionmark.png"
\ 6 Show log - shows the last warnings/error messages (for debugging purposes)
47 *
\ 5img class="toolbarimg intext" src="icons/delete.png"
\ 6 Delete hyperlinks - removes all hyperlinks from the script
49 * If you are new to Matita and/or interactive theorem proving, we have a
50 * tutorial in 10 parts for you. To load it:
51 * 1) click on the "Open script" button in the toolbar (the second circular
52 * button, whose icon shows a folder)
53 * 2) in the dialog box, select the "tutorial/chapter1.ma" script, then
54 * press OK (scripts chapter2.ma ... chapter10.ma contain more advanced
55 * examples that the user is encouraged to try after chapter1.ma)
56 * 3) follow the instructions in the script.