Juliano Cardoso / circusRefine

Blame view

circus/help/en_uk/utils/doc-generator.html 2.18 KB
edit raw normal view history
8d0dc533f   Madiel de Souza Conserva Filho   first 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
 
  <html>
  <head>
      <title>CRefine</title>
      <link rel="stylesheet" type="text/css" href="../../style.css" />
  
  </head>
  
  <body>
  
  <table>
      <tr height="10">
        <td>
        </td>
      </tr>
      <tr>
        <td class="tituloAzul">
          Document Generator
        </td>
      </tr>
      <tr>
        <td class="grande" width="500">
          <br>
          <div align="justify">
          CRefine allows users to produce a final file in .tex format that contains
          all the refinement steps, as well as the proof obligations, the comments, and the
          final code. The comments can be included in the final file before the line it
          has be inserted or a list of comments at the end of the file. This output file cab be used
          in the generation of a pdf file that provides an excellent visualisation of the
          overall refinement.
          <br>
          In order to generate the output file we can click on the button <img border = "0" src="../../../images/print.gif" align="center">
          or choose the Print option in the Development menu.
  
          <br>
          <br>
          <img border = "0" src="../images/doc.jpg" align="center">
          <br>
          <br>
          After selecting Print, a window is shown the user. Using this window, the
          user must select the development items that must be part of the output file. The user
          can also choose the format in which the proof obligation must be included: expanded or contracted.
  
          <br>
          <br>
          <img border = "0" src="../images/doc2.jpg" align="center">
          <br>
          <br>
  
          After confirming the selection by clicking on "OK", a dialog box is shown: the user
          must select the location of the output file and its name. The generated file
          will be in LaTeX format.
          <br>
          <br>
          <img border = "0" src="../images/doc3.jpg" align="center">
          <br>
          <br>
          A message will be given at the end of the generation.
          <br>
          <br>
          <img border = "0" src="../images/doc4.jpg" align="center">
          <br>
          <br>
  
  
          </div>
        </td>
      </tr>
  </table>
  
  
  </body>
  
  </html>