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>