CRefine

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.