]> matita.cs.unibo.it Git - helm.git/commitdiff
Interface change: the get_as_string and set_term methods of the term-editors
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 7 May 2003 11:47:43 +0000 (11:47 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 7 May 2003 11:47:43 +0000 (11:47 +0000)
now work on an unquoted string: the string is TeX quoted (i.e. '$' are
inserted at the beginning and end and '_' are quoted) by set_term and
unquoted by get_as_string. This solves in an almost clean way the
problem of hbugs (that had to quote the string). The solution is maybe still
partial since it is not always possible to serialize/deserialize the input
to a string. An improvement (???) would be to make the output type of
get_as_string opaque and provide two set_term: the first one's input would
be the opaque data type and the second one would be a CIC term.

Changes #54.


No differences found