diff --git a/Data/String/cork.cpp b/Data/String/cork.cpp index 9073f47..7bd1bcf 100644 --- a/Data/String/cork.cpp +++ b/Data/String/cork.cpp @@ -38,28 +38,6 @@ tm_encode (string s) { return r; } -string -tm_decode (string s) { - // TeXmacs encoding to verbatim - int i; - string r; - for (i= 0; i < N (s); i++) { - if (s[i] == '<') { - int j; - for (j= i + 1; j < N (s); j++) - if (s[j] == '>') break; - if (j < N (s)) j++; - if (s (i, j) == "") r << "<"; - else if (s (i, j) == "") r << ">"; - else if (i + 7 == j && s[i + 1] == '#' && s[j - 1] == '>') r << s (i, j); - i= j - 1; - if (s[i] != '>') return r; - } - else if (s[i] != '>') r << s[i]; - } - return r; -} - string tm_var_encode (string s) { int i, n= N (s); @@ -79,6 +57,28 @@ tm_var_encode (string s) { return r; } +string +tm_decode (string s) { + // TeXmacs encoding to verbatim + string r; + int s_N= N (s); + for (int i= 0; i < s_N; i++) { + if (s[i] == '<') { + int j; + for (j= i + 1; j < s_N; j++) + if (s[j] == '>') break; + if (j < s_N) j++; + if (s (i, j) == "") r << "<"; + else if (s (i, j) == "") r << ">"; + else if (i + 7 == j && s[i + 1] == '#' && s[j - 1] == '>') r << s (i, j); + i= j - 1; + if (s[i] != '>') return r; + } + else if (s[i] != '>') r << s[i]; + } + return r; +} + string tm_correct (string s) { int i; diff --git a/tests/Data/String/cork_test.cpp b/tests/Data/String/cork_test.cpp index 3a2bd1a..b90ae82 100644 --- a/tests/Data/String/cork_test.cpp +++ b/tests/Data/String/cork_test.cpp @@ -21,6 +21,20 @@ TEST_CASE ("tm_encode") { string_eq (tm_encode (""), ""); } +TEST_CASE ("tm_var_encode") { + string_eq (tm_var_encode ("<>"), ""); + string_eq (tm_var_encode ("<#ABCD>"), "<#ABCD>"); + string_eq (tm_encode ("abc"), "abc"); + string_eq (tm_encode (""), ""); +} + +TEST_CASE ("tm_decode") { + string_eq (tm_decode (""), "<>"); + string_eq (tm_decode ("<#ABCD>"), "<#ABCD>"); + string_eq (tm_decode ("abc"), "abc"); + string_eq (tm_decode (""), ""); +} + TEST_CASE ("tm_length") { string_eq (tm_string_length (""), 0); string_eq (tm_string_length ("<#ABCD>"), 1);