Xtext，將ascii字符轉換爲數學符號

Question

xtext編輯器如何將乳膠符號\rightarrow翻譯（例如）->？

Answer 1

看一看AUTOEDIT

public class MyDslDefaultAutoEditStrategyProvider extends DefaultAutoEditStrategyProvider { 

    @Inject 
    protected Provider<ShortCutEditStrategy> shortCut; 

    @Override 
    protected void configureStringLiteral(IEditStrategyAcceptor acceptor) { 
     acceptor.accept(shortCut.get().configure("->", "\\rightarrow"), IDocument.DEFAULT_CONTENT_TYPE); 
    } 

} 

的不錯的功能和不要忘了結合

override Class<? extends AbstractEditStrategyProvider> bindAbstractEditStrategyProvider() { 
    MyDslDefaultAutoEditStrategyProvider 
} 

Answer 2

使用JavaScript很容易。這個簡單的腳本應該有所幫助：

replaceText('->', '\rightarrow'); 

var replaceText = function (search, replaceWith) { 
    var area = document.getElementById("area"); 

    var getCount = function (str, search) { 
     return str.split(search).length - 1; 
    }; 
    if (area.value.indexOf(search) >= 0) { 
      var start = area.selectionStart; 
      var end = area.selectionEnd; 
      var textBefore = area.value.substr(0, end); 
      var lengthDiff = (replaceWith.length - search.length) * getCount(textBefore, search); 
      area.value = area.value.replace(search, replaceWith); 
      area.selectionStart = start + lengthDiff; 
      area.selectionEnd = end + lengthDiff; 
     } 
    }; 

此全文可以輕鬆地適應您的使用 - 這裏有一個完整的例子。

<textarea id="area"></textarea> 



<script> 
function keyDownTextField() { 
replaceText('->', '\u2192'); 
} 


var replaceText = function (search, replaceWith) { 
var area = document.getElementById("area"); 

var getCount = function (str, search) { 
    return str.split(search).length - 1; 
}; 

    if (area.value.indexOf(search) >= 0) { 
      var start = area.selectionStart; 
      var end = area.selectionEnd; 
      var textBefore = area.value.substr(0, end); 
      var lengthDiff = (replaceWith.length - search.length) * getCount(textBefore, search); 
      area.value = area.value.replace(search, replaceWith); 
      area.selectionStart = start + lengthDiff; 
      area.selectionEnd = end + lengthDiff; 
     } 
    }; 


    document.addEventListener("keydown", keyDownTextField, false); 

</script>