]> matita.cs.unibo.it Git - helm.git/commit
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)
commit2afbca45037c56264d1889ced69b5f4844b9ecb9
treed7ed43d20b9c06d29e9e0df8bb8997f7341332cd
parent1bfef566743ddd81db375cf66ed3868c5d7df542
Interface change: the get_as_string and set_term methods of the term-editors
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.
helm/gTopLevel/gTopLevel.ml
helm/gTopLevel/hbugs.ml
helm/gTopLevel/termEditor.ml
helm/gTopLevel/termEditor.mli
helm/gTopLevel/texTermEditor.ml
helm/gTopLevel/texTermEditor.mli