aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/wg_ScriptView.ml
diff options
context:
space:
mode:
authorGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-09-30 16:09:56 +0000
committerGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-09-30 16:09:56 +0000
commit698a1ca948794ae9509547ddabd57b5f35512f03 (patch)
tree5d6b6c54d031a25ccc1fcdeafb37bb03416a3e34 /ide/wg_ScriptView.ml
parenta4b5461afbd698b148e11eae003cb4e64bc92af3 (diff)
CoqIDE ported to the revides protocol
- the zone to be edited is now between the marks start_of_input and stop_of_input - when -debug is given, the edit zone is underlined - the cmd_stack is focused/unfocused according to the new protocol - read only tag resurrected and used to block the "Qed" ending a focused zone git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16814 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/wg_ScriptView.ml')
0 files changed, 0 insertions, 0 deletions