Latex/Unicode |
CRefine permite que o programa seja exibido em dois tipos de formato:
LaTeX e Unicode. O formato LaTeX geralmente é mais utilizado no meio
científico. Unicode é um formato mais acessível pois apresenta diretamente
os símbolos que compõe a linguagem Circus.
Durante o carregamento do arquivo LaTeX que representa a especificação inicial, CRefine realiza uma pré-formatação necessária para organizar o programa na tela e facilitar a seleção de termos e conseq^uentemente, todo o processo de refinamento. A alteração do formato de exibição é realizada facilmente sobre a barra de menu, selecionando o tipo de formatação. ![]() Após a seleção da formatação, as janelas de Desenvolvimento, Código e Obrigação de Prova são atualizadas de acordo com a nova formatação. ![]() |