aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/MacOS/default_accel_map376
-rw-r--r--ide/configwin.mli22
-rw-r--r--ide/configwin_ihm.ml220
-rw-r--r--ide/configwin_types.ml6
-rw-r--r--ide/coq.ml8
-rw-r--r--[-rwxr-xr-x]ide/coq2.icobin4710 -> 4710 bytes
-rw-r--r--ide/coqOps.ml55
-rw-r--r--ide/coqOps.mli3
-rw-r--r--ide/coqide.ml73
-rw-r--r--ide/coqide_main.ml5
-rw-r--r--ide/coqide_ui.ml28
-rw-r--r--ide/document.ml18
-rw-r--r--ide/document.mli4
-rw-r--r--ide/gtk_parsing.ml71
-rw-r--r--ide/idetop.ml12
-rw-r--r--ide/ideutils.ml67
-rw-r--r--ide/microPG.ml6
-rw-r--r--ide/minilib.ml20
-rw-r--r--ide/minilib.mli14
-rw-r--r--ide/preferences.ml168
-rw-r--r--ide/preferences.mli3
-rw-r--r--ide/protocol/xml_lexer.mli26
-rw-r--r--ide/session.ml60
-rw-r--r--ide/session.mli2
-rw-r--r--ide/wg_Command.ml6
-rw-r--r--ide/wg_Completion.ml2
-rw-r--r--ide/wg_Find.ml8
-rw-r--r--ide/wg_ScriptView.ml20
28 files changed, 464 insertions, 839 deletions
diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map
deleted file mode 100644
index 54a592a04d..0000000000
--- a/ide/MacOS/default_accel_map
+++ /dev/null
@@ -1,376 +0,0 @@
-; coqide GtkAccelMap rc-file -*- scheme -*-
-; this file is an automated accelerator map dump
-;
-; (gtk_accel_path "<Actions>/Templates/Template Read Module" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic pattern" "")
-(gtk_accel_path "<Actions>/Templates/Definition" "<Shift><Primary>d")
-; (gtk_accel_path "<Actions>/Templates/Template Program Lemma" "")
-(gtk_accel_path "<Actions>/Templates/Lemma" "<Shift><Primary>l")
-; (gtk_accel_path "<Actions>/Templates/Template Fact" "")
-(gtk_accel_path "<Actions>/Tactics/auto" "<Primary><Control>a")
-; (gtk_accel_path "<Actions>/Tactics/Tactic fold" "")
-; (gtk_accel_path "<Actions>/Help/About Coq" "")
-; (gtk_accel_path "<Actions>/Templates/Template Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. " "")
-; (gtk_accel_path "<Actions>/Templates/Template Hypothesis" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic repeat" "")
-; (gtk_accel_path "<Actions>/Templates/Template Unset Extraction Optimize" "")
-; (gtk_accel_path "<Actions>/Templates/Template Add Printing Constructor" "")
-; (gtk_accel_path "<Actions>/Windows/Detach View" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic inversion" "")
-; (gtk_accel_path "<Actions>/Templates/Template Write State" "")
-; (gtk_accel_path "<Actions>/Export/Export to" "")
-(gtk_accel_path "<Actions>/Tactics/auto with *" "<Primary><Control>asterisk")
-; (gtk_accel_path "<Actions>/Tactics/Tactic inversion--clear" "")
-; (gtk_accel_path "<Actions>/Templates/Template Implicit Arguments" "")
-; (gtk_accel_path "<Actions>/Edit/Copy" "<Primary>c")
-; (gtk_accel_path "<Actions>/Tactics/Tactic inversion -- using" "")
-; (gtk_accel_path "<Actions>/View/Previous tab" "<Shift>Left")
-; (gtk_accel_path "<Actions>/Tactics/Tactic change -- in" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic jp" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic red" "")
-; (gtk_accel_path "<Actions>/Templates/Template Coercion" "")
-; (gtk_accel_path "<Actions>/Templates/Template CoFixpoint" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic intros until" "")
-; (gtk_accel_path "<Actions>/Templates/Template Derive Dependent Inversion" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic eapply" "")
-; (gtk_accel_path "<Actions>/View/View" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic change" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic firstorder using" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic decompose sum" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic cut" "")
-; (gtk_accel_path "<Actions>/Templates/Template Remove Printing Let" "")
-; (gtk_accel_path "<Actions>/Templates/Template Structure" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic compute in" "")
-; (gtk_accel_path "<Actions>/Queries/Locate" "")
-; (gtk_accel_path "<Actions>/Templates/Template Save." "")
-; (gtk_accel_path "<Actions>/Templates/Template Canonical Structure" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic compare" "")
-; (gtk_accel_path "<Actions>/Templates/Template Next Obligation" "")
-(gtk_accel_path "<Actions>/View/Display notations" "<Shift><Control>n")
-; (gtk_accel_path "<Actions>/Tactics/Tactic fail" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic left" "")
-(gtk_accel_path "<Actions>/Edit/Undo" "<Primary>u")
-(gtk_accel_path "<Actions>/Tactics/eauto with *" "<Primary><Control>ampersand")
-; (gtk_accel_path "<Actions>/Templates/Template Infix" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic functional induction" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic clear" "")
-; (gtk_accel_path "<Actions>/Templates/Template End Silent." "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic intros" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic constructor -- with" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic destruct" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic intro after" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic abstract" "")
-; (gtk_accel_path "<Actions>/Compile/Compile buffer" "")
-; (gtk_accel_path "<Actions>/Queries/About" "F5")
-; (gtk_accel_path "<Actions>/Templates/Template CoInductive" "")
-; (gtk_accel_path "<Actions>/Templates/Template Test Printing Wildcard" "")
-; (gtk_accel_path "<Actions>/Templates/Template Unset Hyps--limit" "")
-; (gtk_accel_path "<Actions>/Templates/Template Transparent" "")
-; (gtk_accel_path "<Actions>/Export/Ps" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic elim" "")
-; (gtk_accel_path "<Actions>/Templates/Template Extract Constant" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic assert (--:--)" "")
-; (gtk_accel_path "<Actions>/Templates/Template Add Rec LoadPath" "")
-; (gtk_accel_path "<Actions>/Edit/Redo" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic compute" "")
-; (gtk_accel_path "<Actions>/Compile/Next error" "F7")
-; (gtk_accel_path "<Actions>/Templates/Template Add ML Path" "")
-; (gtk_accel_path "<Actions>/Templates/Template Test Printing If" "")
-; (gtk_accel_path "<Actions>/Templates/Template Load Verbose" "")
-; (gtk_accel_path "<Actions>/Templates/Template Reset Extraction Inline" "")
-; (gtk_accel_path "<Actions>/Templates/Template Set Implicit Arguments" "")
-; (gtk_accel_path "<Actions>/Templates/Template Test Printing Let" "")
-; (gtk_accel_path "<Actions>/Windows/Windows" "")
-; (gtk_accel_path "<Actions>/Templates/Template Defined." "")
-(gtk_accel_path "<Actions>/Templates/match" "<Shift><Primary>c")
-; (gtk_accel_path "<Actions>/Tactics/Tactic set (--:=--)" "")
-; (gtk_accel_path "<Actions>/Templates/Template Proof." "")
-; (gtk_accel_path "<Actions>/Compile/Make" "F6")
-; (gtk_accel_path "<Actions>/Templates/Template Module Type" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic apply -- with" "")
-; (gtk_accel_path "<Actions>/File/Save as" "")
-; (gtk_accel_path "<Actions>/Templates/Template Set Hyps--limit" "")
-; (gtk_accel_path "<Actions>/Templates/Template Global Variable" "")
-; (gtk_accel_path "<Actions>/Templates/Template Remove Printing Constructor" "")
-; (gtk_accel_path "<Actions>/Templates/Template Add Setoid" "")
-; (gtk_accel_path "<Actions>/Edit/Find Next" "F3")
-; (gtk_accel_path "<Actions>/Edit/Find" "<Primary>f")
-; (gtk_accel_path "<Actions>/Templates/Template Add Relation" "")
-; (gtk_accel_path "<Actions>/Queries/Print" "F4")
-; (gtk_accel_path "<Actions>/Templates/Template Obligations Tactic" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic trivial" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic first" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic case" "")
-; (gtk_accel_path "<Actions>/Templates/Template Hint Constructors" "")
-; (gtk_accel_path "<Actions>/Templates/Template Add Abstract Ring A Aplus Amult Aone Azero Ainv Aeq T." "")
-; (gtk_accel_path "<Actions>/Templates/Template Coercion Local" "")
-(gtk_accel_path "<Actions>/View/Show Query Pane" "<Control>Escape")
-; (gtk_accel_path "<Actions>/Tactics/Tactic cbv" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic inversion--clear -- in" "")
-; (gtk_accel_path "<Actions>/Templates/Template Add Rec ML Path" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic apply" "")
-; (gtk_accel_path "<Actions>/Export/Latex" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic inversion -- using -- in" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic generalize" "")
-(gtk_accel_path "<Actions>/Navigation/Backward" "<Primary><Control>Up")
-; (gtk_accel_path "<Actions>/Tactics/Tactic p" "")
-(gtk_accel_path "<Actions>/Navigation/Hide" "<Primary><Control>h")
-; (gtk_accel_path "<Actions>/File/Close buffer" "<Primary>w")
-; (gtk_accel_path "<Actions>/Tactics/Tactic induction" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic eauto with" "")
-(gtk_accel_path "<Actions>/View/Display raw matching expressions" "<Shift><Control>m")
-; (gtk_accel_path "<Actions>/Tactics/Tactic d" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic u" "")
-; (gtk_accel_path "<Actions>/Templates/Templates" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic s" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic lapply" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic t" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic r" "")
-; (gtk_accel_path "<Actions>/Edit/Replace" "<Primary>r")
-; (gtk_accel_path "<Actions>/Tactics/Tactic case -- with" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic eexact" "")
-; (gtk_accel_path "<Actions>/Queries/Check" "F3")
-; (gtk_accel_path "<Actions>/Tactics/Tactic omega" "")
-; (gtk_accel_path "<Actions>/File/New" "<Primary>n")
-; (gtk_accel_path "<Actions>/Tactics/Tactic l" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic intro" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic j" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic i" "")
-; (gtk_accel_path "<Actions>/Templates/Template Definition" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic g" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic f" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic e" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic c" "")
-(gtk_accel_path "<Actions>/File/Rehighlight" "<Primary>l")
-; (gtk_accel_path "<Actions>/Tactics/Tactic simple inversion" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic a" "")
-; (gtk_accel_path "<Actions>/Templates/Template Mutual Inductive" "")
-; (gtk_accel_path "<Actions>/Templates/Template Extraction NoInline" "")
-(gtk_accel_path "<Actions>/Templates/Theorem" "<Shift><Primary>t")
-; (gtk_accel_path "<Actions>/Templates/Template Derive Dependent Inversion--clear" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic unfold" "")
-; (gtk_accel_path "<Actions>/Tactics/Try Tactics" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic red in" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite <- -- in" "")
-; (gtk_accel_path "<Actions>/Templates/Template Hint Extern" "")
-; (gtk_accel_path "<Actions>/Templates/Template Unfocus" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic dependent inversion--clear" "")
-; (gtk_accel_path "<Actions>/Help/Browse Coq Library" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic lazy" "")
-; (gtk_accel_path "<Actions>/Templates/Template Scheme" "")
-(gtk_accel_path "<Actions>/Tactics/tauto" "<Primary><Control>p")
-; (gtk_accel_path "<Actions>/Tactics/Tactic cutrewrite" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic contradiction" "")
-; (gtk_accel_path "<Actions>/Templates/Template Set Printing Wildcard" "")
-; (gtk_accel_path "<Actions>/Templates/Template Add LoadPath" "")
-(gtk_accel_path "<Actions>/Navigation/Previous" "<Primary><Control>less")
-; (gtk_accel_path "<Actions>/Templates/Template Require" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic simpl" "")
-; (gtk_accel_path "<Actions>/Templates/Template Require Import" "")
-; (gtk_accel_path "<Actions>/Templates/Template Add Abstract Semi Ring A Aplus Amult Aone Azero Aeq T." "")
-(gtk_accel_path "<Actions>/Navigation/Forward" "<Primary><Control>Down")
-; (gtk_accel_path "<Actions>/Tactics/Tactic rename -- into" "")
-; (gtk_accel_path "<Actions>/Compile/Compile" "")
-; (gtk_accel_path "<Actions>/File/Save all" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic fix" "")
-; (gtk_accel_path "<Actions>/Templates/Template Parameter" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic assert" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic do" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic ring" "")
-; (gtk_accel_path "<Actions>/Export/Pdf" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic quote" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic symmetry in" "")
-; (gtk_accel_path "<Actions>/Help/Help" "")
-(gtk_accel_path "<Actions>/Templates/Inductive" "<Shift><Primary>i")
-; (gtk_accel_path "<Actions>/Tactics/Tactic idtac" "")
-; (gtk_accel_path "<Actions>/Templates/Template Syntax" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic intro -- after" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic fold -- in" "")
-; (gtk_accel_path "<Actions>/Templates/Template Program Definition" "")
-(gtk_accel_path "<Actions>/Tactics/Wizard" "<Primary><Control>dollar")
-; (gtk_accel_path "<Actions>/Templates/Template Hint Resolve" "")
-; (gtk_accel_path "<Actions>/Templates/Template Set Extraction Optimize" "")
-; (gtk_accel_path "<Actions>/File/Revert all buffers" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic subst" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic autorewrite" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic pose" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic simplify--eq" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic clearbody" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic eauto" "")
-; (gtk_accel_path "<Actions>/Templates/Template Grammar" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic exact" "")
-; (gtk_accel_path "<Actions>/Templates/Template Unset Implicit Arguments" "")
-; (gtk_accel_path "<Actions>/Templates/Template Extract Inductive" "")
-(gtk_accel_path "<Actions>/View/Display implicit arguments" "<Shift><Control>i")
-; (gtk_accel_path "<Actions>/Tactics/Tactic symmetry" "")
-; (gtk_accel_path "<Actions>/Templates/Template Add Printing Let" "")
-; (gtk_accel_path "<Actions>/Help/Help for keyword" "<Primary>h")
-; (gtk_accel_path "<Actions>/File/Save" "<Primary>s")
-; (gtk_accel_path "<Actions>/Compile/Make makefile" "")
-; (gtk_accel_path "<Actions>/Templates/Template Remove LoadPath" "")
-(gtk_accel_path "<Actions>/Navigation/Interrupt" "<Primary><Control>Break")
-(gtk_accel_path "<Actions>/Navigation/End" "<Primary><Control>End")
-; (gtk_accel_path "<Actions>/Templates/Template Add Morphism" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic field" "")
-; (gtk_accel_path "<Actions>/Templates/Template Axiom" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic solve" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic casetype" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic cbv in" "")
-; (gtk_accel_path "<Actions>/Templates/Template Load" "")
-; (gtk_accel_path "<Actions>/Templates/Template Goal" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic exists" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic decompose record" "")
-(gtk_accel_path "<Actions>/Navigation/Go to" "<Primary><Control>Right")
-; (gtk_accel_path "<Actions>/Templates/Template Remark" "")
-; (gtk_accel_path "<Actions>/Templates/Template Set Undo" "")
-; (gtk_accel_path "<Actions>/Templates/Template Inductive" "")
-(gtk_accel_path "<Actions>/Edit/Preferences" "<Primary>VoidSymbol")
-; (gtk_accel_path "<Actions>/Export/Html" "")
-; (gtk_accel_path "<Actions>/Templates/Template Extraction Inline" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic absurd" "")
-(gtk_accel_path "<Actions>/Tactics/intuition" "<Primary><Control>i")
-; (gtk_accel_path "<Actions>/Tactics/Tactic simple induction" "")
-; (gtk_accel_path "<Actions>/Queries/Queries" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite -- in" "")
-; (gtk_accel_path "<Actions>/Templates/Template Hint Rewrite" "")
-; (gtk_accel_path "<Actions>/Templates/Template Add Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ]." "")
-; (gtk_accel_path "<Actions>/Navigation/Navigation" "")
-; (gtk_accel_path "<Actions>/Help/Browse Coq Manual" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic transitivity" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic auto" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic dependent inversion -- with" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic assumption" "")
-; (gtk_accel_path "<Actions>/Templates/Template Notation" "")
-; (gtk_accel_path "<Actions>/Edit/Cut" "<Primary>x")
-; (gtk_accel_path "<Actions>/Templates/Template Theorem" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic constructor" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic elim -- with" "")
-; (gtk_accel_path "<Actions>/Templates/Template Identity Coercion" "")
-(gtk_accel_path "<Actions>/View/Display all low-level contents" "<Shift><Control>l")
-; (gtk_accel_path "<Actions>/Tactics/Tactic right" "")
-; (gtk_accel_path "<Actions>/Edit/Find Previous" "<Shift>F3")
-; (gtk_accel_path "<Actions>/Tactics/Tactic cofix" "")
-; (gtk_accel_path "<Actions>/Templates/Template Restore State" "")
-; (gtk_accel_path "<Actions>/Templates/Template Lemma" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic refine" "")
-; (gtk_accel_path "<Actions>/Templates/Template Section" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic assert (--:=--)" "")
-; (gtk_accel_path "<Actions>/Templates/Template Unset Printing Wildcard" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic progress" "")
-; (gtk_accel_path "<Actions>/Templates/Template Add Printing If" "")
-; (gtk_accel_path "<Actions>/Templates/Template Chapter" "")
-(gtk_accel_path "<Actions>/File/Print..." "<Primary>p")
-; (gtk_accel_path "<Actions>/Templates/Template Record" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic info" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic firstorder with" "")
-; (gtk_accel_path "<Actions>/Templates/Template Hint Unfold" "")
-; (gtk_accel_path "<Actions>/Templates/Template Set Silent." "")
-; (gtk_accel_path "<Actions>/Templates/Template Program Theorem" "")
-; (gtk_accel_path "<Actions>/Templates/Template Declare ML Module" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic lazy in" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic unfold -- in" "")
-; (gtk_accel_path "<Actions>/Edit/Paste" "<Primary>v")
-; (gtk_accel_path "<Actions>/Templates/Template Remove Printing If" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic intuition" "")
-; (gtk_accel_path "<Actions>/Queries/SearchAbout" "F2")
-; (gtk_accel_path "<Actions>/Tactics/Tactic dependent rewrite ->" "")
-; (gtk_accel_path "<Actions>/Templates/Template Module" "")
-; (gtk_accel_path "<Actions>/Templates/Template Unset Extraction AutoInline" "")
-(gtk_accel_path "<Actions>/Templates/Scheme" "<Shift><Primary>s")
-; (gtk_accel_path "<Actions>/Templates/Template V" "")
-; (gtk_accel_path "<Actions>/Templates/Template Variable" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic decide equality" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic instantiate (--:=--)" "")
-; (gtk_accel_path "<Actions>/Templates/Template Syntactic Definition" "")
-; (gtk_accel_path "<Actions>/Templates/Template Set Extraction AutoInline" "")
-; (gtk_accel_path "<Actions>/Templates/Template Unset Undo" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic dependent inversion" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic setoid--rewrite" "")
-; (gtk_accel_path "<Actions>/Templates/Template Add Field" "")
-; (gtk_accel_path "<Actions>/Templates/Template Require Export" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite <-" "")
-(gtk_accel_path "<Actions>/Tactics/omega" "<Primary><Control>o")
-; (gtk_accel_path "<Actions>/Tactics/Tactic split" "")
-; (gtk_accel_path "<Actions>/File/Quit" "<Primary>q")
-(gtk_accel_path "<Actions>/View/Display existential variable instances" "<Shift><Control>e")
-(gtk_accel_path "<Actions>/Navigation/Start" "<Primary><Control>Home")
-; (gtk_accel_path "<Actions>/Tactics/Tactic dependent rewrite <-" "")
-; (gtk_accel_path "<Actions>/Templates/Template U" "")
-; (gtk_accel_path "<Actions>/Templates/Template Variables" "")
-; (gtk_accel_path "<Actions>/Templates/Template S" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic move -- after" "")
-; (gtk_accel_path "<Actions>/Templates/Template Unset Silent." "")
-; (gtk_accel_path "<Actions>/Templates/Template Local" "")
-; (gtk_accel_path "<Actions>/Templates/Template T" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic reflexivity" "")
-; (gtk_accel_path "<Actions>/Templates/Template R" "")
-; (gtk_accel_path "<Actions>/Templates/Template Time" "")
-; (gtk_accel_path "<Actions>/Templates/Template P" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic decompose" "")
-; (gtk_accel_path "<Actions>/Templates/Template N" "")
-; (gtk_accel_path "<Actions>/Templates/Template Eval" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic congruence" "")
-; (gtk_accel_path "<Actions>/Templates/Template O" "")
-; (gtk_accel_path "<Actions>/Templates/Template E" "")
-; (gtk_accel_path "<Actions>/Templates/Template I" "")
-; (gtk_accel_path "<Actions>/Templates/Template H" "")
-; (gtk_accel_path "<Actions>/Templates/Template Extraction Language" "")
-; (gtk_accel_path "<Actions>/Templates/Template M" "")
-; (gtk_accel_path "<Actions>/Templates/Template Derive Inversion" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic double induction" "")
-; (gtk_accel_path "<Actions>/Templates/Template L" "")
-; (gtk_accel_path "<Actions>/Templates/Template Derive Inversion--clear" "")
-(gtk_accel_path "<Actions>/View/Display universe levels" "<Shift><Control>u")
-; (gtk_accel_path "<Actions>/Templates/Template G" "")
-; (gtk_accel_path "<Actions>/Templates/Template F" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic dependent inversion--clear -- with" "")
-; (gtk_accel_path "<Actions>/Templates/Template D" "")
-; (gtk_accel_path "<Actions>/Edit/Edit" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic firstorder" "")
-; (gtk_accel_path "<Actions>/Templates/Template C" "")
-(gtk_accel_path "<Actions>/Tactics/simpl" "<Primary><Control>s")
-; (gtk_accel_path "<Actions>/Tactics/Tactic replace -- with" "")
-; (gtk_accel_path "<Actions>/Templates/Template A" "")
-; (gtk_accel_path "<Actions>/Templates/Template Remove Printing Record" "")
-; (gtk_accel_path "<Actions>/Templates/Template Qed." "")
-; (gtk_accel_path "<Actions>/Templates/Template Program Fixpoint" "")
-(gtk_accel_path "<Actions>/View/Display coercions" "<Shift><Control>c")
-; (gtk_accel_path "<Actions>/Tactics/Tactic hnf" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic injection" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite" "")
-; (gtk_accel_path "<Actions>/Templates/Template Opaque" "")
-; (gtk_accel_path "<Actions>/Templates/Template Focus" "")
-; (gtk_accel_path "<Actions>/Templates/Template Ltac" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic simple destruct" "")
-(gtk_accel_path "<Actions>/View/Display all basic low-level contents" "<Shift><Control>a")
-; (gtk_accel_path "<Actions>/Tactics/Tactic jp <n>" "")
-; (gtk_accel_path "<Actions>/Templates/Template Test Printing Synth" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic set" "")
-; (gtk_accel_path "<Actions>/Edit/External editor" "")
-; (gtk_accel_path "<Actions>/View/Show Toolbar" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic try" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic discriminate" "")
-(gtk_accel_path "<Actions>/Templates/Fixpoint" "<Shift><Primary>f")
-(gtk_accel_path "<Actions>/Edit/Complete Word" "<Primary>slash")
-(gtk_accel_path "<Actions>/Navigation/Next" "<Primary><Control>greater")
-; (gtk_accel_path "<Actions>/Tactics/Tactic elimtype" "")
-; (gtk_accel_path "<Actions>/Templates/Template End" "")
-; (gtk_accel_path "<Actions>/Templates/Template Fixpoint" "")
-; (gtk_accel_path "<Actions>/View/Next tab" "<Shift>Right")
-; (gtk_accel_path "<Actions>/File/File" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic setoid--replace" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic generalize dependent" "")
-(gtk_accel_path "<Actions>/Tactics/trivial" "<Primary><Control>v")
-; (gtk_accel_path "<Actions>/Tactics/Tactic fix -- with" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic pose --:=--)" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic auto with" "")
-; (gtk_accel_path "<Actions>/Templates/Template Add Printing Record" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic inversion -- in" "")
-(gtk_accel_path "<Actions>/Tactics/eauto" "<Primary><Control>e")
-; (gtk_accel_path "<Actions>/File/Open" "<Primary>o")
-; (gtk_accel_path "<Actions>/Tactics/Tactic elim -- using" "")
-; (gtk_accel_path "<Actions>/Templates/Template Hint" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic tauto" "")
-; (gtk_accel_path "<Actions>/Export/Dvi" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic simpl -- in" "")
-; (gtk_accel_path "<Actions>/Templates/Template Hint Immediate" "")
diff --git a/ide/configwin.mli b/ide/configwin.mli
index fa22846d19..b5c3e74aec 100644
--- a/ide/configwin.mli
+++ b/ide/configwin.mli
@@ -42,13 +42,13 @@ type configuration_structure =
type return_button =
Return_apply
(** The user clicked on Apply at least once before
- closing the window with Cancel or the window manager. *)
+ closing the window with Cancel or the window manager. *)
| Return_ok
(** The user closed the window with the ok button. *)
| Return_cancel
(** The user closed the window with the cancel
- button or the window manager but never clicked
- on the apply button.*)
+ button or the window manager but never clicked
+ on the apply button.*)
(** {2 Functions to create parameters} *)
@@ -84,7 +84,7 @@ val strings : ?editable: bool -> ?help: string ->
?f: (string list -> unit) ->
?eq: (string -> string -> bool) ->
?add: (unit -> string list) ->
- string -> string list -> parameter_kind
+ string -> string list -> parameter_kind
(** [list label f_strings value] creates a list parameter.
[f_strings] is a function taking a value and returning a list
@@ -113,13 +113,13 @@ val list : ?editable: bool -> ?help: string ->
?f: ('a list -> unit) ->
?eq: ('a -> 'a -> bool) ->
?edit: ('a -> 'a) ->
- ?add: (unit -> 'a list) ->
- ?titles: string list ->
- ?color: ('a -> string option) ->
- string ->
- ('a -> string list) ->
- 'a list ->
- parameter_kind
+ ?add: (unit -> 'a list) ->
+ ?titles: string list ->
+ ?color: ('a -> string option) ->
+ string ->
+ ('a -> string list) ->
+ 'a list ->
+ parameter_kind
*)
(** [combo label choices value] creates a combo parameter.
diff --git a/ide/configwin_ihm.ml b/ide/configwin_ihm.ml
index 0f3fd38a7a..e768131dcf 100644
--- a/ide/configwin_ihm.ml
+++ b/ide/configwin_ihm.ml
@@ -38,15 +38,15 @@ let modifiers_to_string m =
| c :: m ->
iter m ((
match c with
- `CONTROL -> "<ctrl>"
- | `SHIFT -> "<shft>"
- | `LOCK -> "<lock>"
- | `MOD1 -> "<alt>"
- | `MOD2 -> "<mod2>"
- | `MOD3 -> "<mod3>"
- | `MOD4 -> "<mod4>"
- | `MOD5 -> "<mod5>"
- | _ -> raise Not_found
+ `CONTROL -> "<ctrl>"
+ | `SHIFT -> "<shft>"
+ | `LOCK -> "<lock>"
+ | `MOD1 -> "<alt>"
+ | `MOD2 -> "<mod2>"
+ | `MOD3 -> "<mod3>"
+ | `MOD4 -> "<mod4>"
+ | `MOD5 -> "<mod5>"
+ | _ -> raise Not_found
) ^ s)
in
iter m ""
@@ -89,13 +89,13 @@ class ['a] list_selection_box
let wlist = match titles_opt with
None ->
GList.clist ~selection_mode: `MULTIPLE
- ~titles_show: false
- ~packing: wscroll#add ()
+ ~titles_show: false
+ ~packing: wscroll#add ()
| Some l ->
GList.clist ~selection_mode: `MULTIPLE
- ~titles: l
- ~titles_show: true
- ~packing: wscroll#add ()
+ ~titles: l
+ ~titles_show: true
+ ~packing: wscroll#add ()
in
let _ = set_help_tip wev help_opt in
(* the vbox for the buttons *)
@@ -146,18 +146,18 @@ class ['a] list_selection_box
wlist#freeze ();
wlist#clear ();
List.iter
- (fun ele ->
- ignore (wlist#append (f_strings ele));
- match f_color ele with
- None -> ()
- | Some c ->
- try wlist#set_row ~foreground: (`NAME c) (wlist#rows - 1)
- with _ -> ()
- )
- !listref;
+ (fun ele ->
+ ignore (wlist#append (f_strings ele));
+ match f_color ele with
+ None -> ()
+ | Some c ->
+ try wlist#set_row ~foreground: (`NAME c) (wlist#rows - 1)
+ with _ -> ()
+ )
+ !listref;
(match titles_opt with
- None -> wlist#columns_autosize ()
+ None -> wlist#columns_autosize ()
| Some _ -> GToolbox.autosize_clist wlist);
wlist#thaw ();
(* the list of selectd elements is now empty *)
@@ -166,18 +166,18 @@ class ['a] list_selection_box
(** Move up the selected rows. *)
method up_selected =
let rec iter n selrows l =
- match selrows with
- [] -> (l, [])
- | m :: qrows ->
- match l with
- [] -> ([],[])
- | [_] -> (l,[])
- | e1 :: e2 :: q when m = n + 1 ->
- let newl, newrows = iter (n+1) qrows (e1 :: q) in
- (e2 :: newl, n :: newrows)
- | e1 :: q ->
- let newl, newrows = iter (n+1) selrows q in
- (e1 :: newl, newrows)
+ match selrows with
+ [] -> (l, [])
+ | m :: qrows ->
+ match l with
+ [] -> ([],[])
+ | [_] -> (l,[])
+ | e1 :: e2 :: q when m = n + 1 ->
+ let newl, newrows = iter (n+1) qrows (e1 :: q) in
+ (e2 :: newl, n :: newrows)
+ | e1 :: q ->
+ let newl, newrows = iter (n+1) selrows q in
+ (e1 :: newl, newrows)
in
let sorted_select = List.sort compare list_select in
let new_list, new_rows = iter 0 sorted_select !listref in
@@ -188,24 +188,24 @@ class ['a] list_selection_box
method edit_selected f_edit =
let sorted_select = List.sort compare list_select in
match sorted_select with
- [] -> ()
+ [] -> ()
| n :: _ ->
- try
- let ele = List.nth !listref n in
- let ele2 = f_edit ele in
- let rec iter m = function
- [] -> []
- | e :: q ->
- if n = m then
- ele2 :: q
- else
- e :: (iter (m+1) q)
- in
- self#update (iter 0 !listref);
- wlist#select n 0
- with
- Not_found ->
- ()
+ try
+ let ele = List.nth !listref n in
+ let ele2 = f_edit ele in
+ let rec iter m = function
+ [] -> []
+ | e :: q ->
+ if n = m then
+ ele2 :: q
+ else
+ e :: (iter (m+1) q)
+ in
+ self#update (iter 0 !listref);
+ wlist#select n 0
+ with
+ Not_found ->
+ ()
initializer
@@ -228,14 +228,14 @@ class ['a] list_selection_box
in
let f_remove () =
(* remove the selected items from the listref and the clist *)
- let rec iter n = function
- [] -> []
- | h :: q ->
- if List.mem n list_select then
- iter (n+1) q
- else
- h :: (iter (n+1) q)
- in
+ let rec iter n = function
+ [] -> []
+ | h :: q ->
+ if List.mem n list_select then
+ iter (n+1) q
+ else
+ h :: (iter (n+1) q)
+ in
let new_list = iter 0 !listref in
self#update new_list
in
@@ -248,10 +248,10 @@ class ['a] list_selection_box
ignore (wb_up#connect#clicked ~callback:(fun () -> self#up_selected));
(
match f_edit_opt with
- None -> ()
+ None -> ()
| Some f ->
- let _ = dbg "list_selection_box: connecting wb_edit" in
- ignore (wb_edit#connect#clicked ~callback:(fun () -> self#edit_selected f))
+ let _ = dbg "list_selection_box: connecting wb_edit" in
+ ignore (wb_edit#connect#clicked ~callback:(fun () -> self#edit_selected f))
);
(* connect the selection and deselection of items in the clist *)
let f_select ~row ~column ~event =
@@ -303,10 +303,10 @@ class string_param_box param =
method apply =
let new_value = param.string_of_string we#text in
if new_value <> param.string_value then
- let _ = param.string_f_apply new_value in
- param.string_value <- new_value
+ let _ = param.string_f_apply new_value in
+ param.string_value <- new_value
else
- ()
+ ()
end ;;
(** This class is used to build a box for a combo parameter.*)
@@ -318,16 +318,16 @@ class combo_param_box param =
let _ = set_help_tip wev param.combo_help in
let get_value = if not param.combo_new_allowed then
let wc = GEdit.combo_box_text
- ~strings: param.combo_choices
- ?active:(let rec aux i = function
- |[] -> None
- |h::_ when h = param.combo_value -> Some i
- |_::t -> aux (succ i) t
- in aux 0 param.combo_choices)
- ~packing: (hbox#pack ~expand: param.combo_expand ~padding: 2)
- ()
+ ~strings: param.combo_choices
+ ?active:(let rec aux i = function
+ |[] -> None
+ |h::_ when h = param.combo_value -> Some i
+ |_::t -> aux (succ i) t
+ in aux 0 param.combo_choices)
+ ~packing: (hbox#pack ~expand: param.combo_expand ~padding: 2)
+ ()
in
- fun () -> match GEdit.text_combo_get_active wc with |None -> "" |Some s -> s
+ fun () -> match GEdit.text_combo_get_active wc with |None -> "" |Some s -> s
else
let (wc,_) = GEdit.combo_box_entry_text
~strings: param.combo_choices
@@ -347,10 +347,10 @@ object (self)
method apply =
let new_value = get_value () in
if new_value <> param.combo_value then
- let _ = param.combo_f_apply new_value in
- param.combo_value <- new_value
+ let _ = param.combo_f_apply new_value in
+ param.combo_value <- new_value
else
- ()
+ ()
end ;;
(** Class used to pack a custom box. *)
@@ -360,9 +360,9 @@ class custom_param_box param =
match param.custom_framed with
None -> param.custom_box#coerce
| Some l ->
- let wf = GBin.frame ~label: l () in
- wf#add param.custom_box#coerce;
- wf#coerce
+ let wf = GBin.frame ~label: l () in
+ wf#add param.custom_box#coerce;
+ wf#coerce
in
object (self)
method box = top
@@ -401,13 +401,13 @@ class text_param_box param =
method apply =
let v = param.string_of_string (buffer#get_text ()) in
if v <> param.string_value then
- (
- dbg "apply new value!";
- let _ = param.string_f_apply v in
- param.string_value <- v
- )
+ (
+ dbg "apply new value!";
+ let _ = param.string_f_apply v in
+ param.string_value <- v
+ )
else
- ()
+ ()
end ;;
(** This class is used to build a box for a boolean parameter.*)
@@ -430,10 +430,10 @@ class bool_param_box param =
method apply =
let new_value = wchk#active in
if new_value <> param.bool_value then
- let _ = param.bool_f_apply new_value in
- param.bool_value <- new_value
+ let _ = param.bool_f_apply new_value in
+ param.bool_value <- new_value
else
- ()
+ ()
end ;;
class modifiers_param_box param =
@@ -461,10 +461,10 @@ class modifiers_param_box param =
method apply =
let new_value = !value in
if new_value <> param.md_value then
- let _ = param.md_f_apply new_value in
- param.md_value <- new_value
+ let _ = param.md_f_apply new_value in
+ param.md_value <- new_value
else
- ()
+ ()
end ;;
(*
(** This class is used to build a box for a parameter whose values are a list.*)
@@ -728,20 +728,20 @@ let list ?(editable=true) ?help
label (f_strings : 'a -> string list) v =
List_param
(fun () ->
- new list_param_box
- {
- list_label = label ;
- list_help = help ;
- list_value = v ;
- list_editable = editable ;
- list_titles = titles;
- list_eq = eq ;
- list_strings = f_strings ;
- list_color = color ;
- list_f_edit = edit ;
- list_f_add = add ;
- list_f_apply = f ;
- }
+ new list_param_box
+ {
+ list_label = label ;
+ list_help = help ;
+ list_value = v ;
+ list_editable = editable ;
+ list_titles = titles;
+ list_eq = eq ;
+ list_strings = f_strings ;
+ list_color = color ;
+ list_f_edit = edit ;
+ list_f_add = add ;
+ list_f_apply = f ;
+ }
)
(** Create a strings param. *)
@@ -818,10 +818,10 @@ let question_box ~title ~buttons ?(default=1) ?icon ?parent message =
in
ignore (b#connect#clicked ~callback:
(fun () -> button_nb := n; window#destroy ()));
- (* If it's the first button then give it the focus *)
+ (* If it's the first button then give it the focus *)
if n = default then b#grab_default () else ();
- iter_buttons (n+1) q
+ iter_buttons (n+1) q
in
iter_buttons 1 buttons;
ignore (window#connect#destroy ~callback: GMain.Main.quit);
diff --git a/ide/configwin_types.ml b/ide/configwin_types.ml
index 4c66a6944e..711eccd08e 100644
--- a/ide/configwin_types.ml
+++ b/ide/configwin_types.ml
@@ -114,8 +114,8 @@ type configuration_structure =
(** To indicate what button was pushed by the user when the window is closed. *)
type return_button =
Return_apply (** The user clicked on Apply at least once before
- closing the window with Cancel or the window manager. *)
+ closing the window with Cancel or the window manager. *)
| Return_ok (** The user closed the window with the ok button. *)
| Return_cancel (** The user closed the window with the cancel
- button or the window manager but never clicked
- on the apply button.*)
+ button or the window manager but never clicked
+ on the apply button.*)
diff --git a/ide/coq.ml b/ide/coq.ml
index 889cc3be36..4d6ba55d76 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -56,7 +56,7 @@ let rec read_all_lines in_chan =
let len = String.length arg in
let arg =
if len > 0 && arg.[len - 1] = '\r' then
- String.sub arg 0 (len - 1)
+ String.sub arg 0 (len - 1)
else arg
in
arg::(read_all_lines in_chan)
@@ -135,7 +135,7 @@ and asks_for_coqtop args =
match file with
| Some _ ->
let () = custom_coqtop := file in
- filter_coq_opts args
+ filter_coq_opts args
| None -> exit 0
exception WrongExitStatus of string
@@ -597,8 +597,8 @@ struct
let opts = Hashtbl.fold mkopt current_state [] in
eval_call (Xmlprotocol.set_options opts) h
(function
- | Interface.Good () -> k ()
- | _ -> failwith "Cannot set options. Resetting coqtop")
+ | Interface.Good () -> k ()
+ | _ -> failwith "Cannot set options. Resetting coqtop")
end
diff --git a/ide/coq2.ico b/ide/coq2.ico
index bc1732fd99..bc1732fd99 100755..100644
--- a/ide/coq2.ico
+++ b/ide/coq2.ico
Binary files differ
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 566654218d..89425bda56 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -137,7 +137,6 @@ class type ops =
object
method go_to_insert : unit task
method go_to_mark : GText.mark -> unit task
- method tactic_wizard : string list -> unit task
method process_next_phrase : unit task
method process_until_end_or_error : unit task
method handle_reset_initial : unit task
@@ -281,7 +280,7 @@ object(self)
List.exists (fun m ->
Gobject.get_oid m =
Gobject.get_oid (buffer#get_mark s.start)) marks in
- try Doc.find document mem_marks
+ try Doc.find document mem_marks
with Not_found -> aux iter#backward_char in
aux iter in
let ss =
@@ -294,7 +293,7 @@ object(self)
script#misc#set_tooltip_text ""; script#misc#set_has_tooltip true
end;
false
-
+
method destroy () =
feedback_timer.Ideutils.kill ()
@@ -324,7 +323,7 @@ object(self)
method private get_start_of_input =
buffer#get_iter_at_mark (`NAME "start_of_input")
-
+
method private get_end_of_input =
buffer#get_iter_at_mark (`NAME "stop_of_input")
@@ -698,7 +697,7 @@ object(self)
method private find_id until =
try
Doc.find_id document (fun id { start;stop } -> until (Some id) start stop)
- with Not_found -> initial_state, Doc.focused document
+ with Not_found -> initial_state, Doc.focused document
method private cleanup seg =
if seg <> [] then begin
@@ -759,7 +758,7 @@ object(self)
(Doc.focused document && Doc.is_in_focus document safe_id))
in
undo to_id unfocus_needed)
-
+
method private backtrack_until ?move_insert until =
self#backtrack_to_id ?move_insert (self#find_id until)
@@ -783,7 +782,7 @@ object(self)
method backtrack_last_phrase =
messages#default_route#clear;
- try
+ try
let tgt = Doc.before_tip document in
self#backtrack_to_id tgt
with Not_found -> Coq.return (Coq.reset_coqtop _ct)
@@ -806,48 +805,6 @@ object(self)
else Coq.seq (self#backtrack_to_iter ~move_insert:false point)
(Coq.lift (fun () -> Sentence.tag_on_insert buffer)))
- method tactic_wizard l =
- let insert_phrase phrase tag =
- let stop = self#get_start_of_input in
- let phrase' = if stop#starts_line then phrase else "\n"^phrase in
- buffer#insert ~iter:stop phrase';
- Sentence.tag_on_insert buffer;
- let start = self#get_start_of_input in
- buffer#move_mark ~where:stop (`NAME "start_of_input");
- buffer#apply_tag tag ~start ~stop;
- if self#get_insert#compare stop <= 0 then
- buffer#place_cursor ~where:stop;
- let sentence =
- mk_sentence
- ~start:(`MARK (buffer#create_mark start))
- ~stop:(`MARK (buffer#create_mark stop))
- [] in
- Doc.push document sentence;
- messages#default_route#clear;
- self#show_goals
- in
- let display_error (loc, s) =
- messages#default_route#add (Ideutils.validate s) in
- let try_phrase phrase stop more =
- let action = log "Sending to coq now" in
- let route_id = 0 in
- let query = Coq.query (route_id,(phrase,Stateid.dummy)) in
- let next = function
- | Fail (_, l, str) -> (* FIXME: check *)
- display_error (l, str);
- messages#default_route#add (Pp.str ("Unsuccessfully tried: "^phrase));
- more
- | Good () -> stop Tags.Script.processed
- in
- Coq.bind (Coq.seq action query) next
- in
- let rec loop l = match l with
- | [] -> Coq.return ()
- | p :: l' ->
- try_phrase ("progress "^p^".") (insert_phrase (p^".")) (loop l')
- in
- loop l
-
method handle_reset_initial =
let action () =
(* clear the stack *)
diff --git a/ide/coqOps.mli b/ide/coqOps.mli
index 83ad8c15dc..58d69c0aaa 100644
--- a/ide/coqOps.mli
+++ b/ide/coqOps.mli
@@ -15,7 +15,6 @@ class type ops =
object
method go_to_insert : unit task
method go_to_mark : GText.mark -> unit task
- method tactic_wizard : string list -> unit task
method process_next_phrase : unit task
method process_until_end_or_error : unit task
method handle_reset_initial : unit task
@@ -33,7 +32,7 @@ object
method handle_failure : handle_exn_rty -> unit task
-
+
method destroy : unit -> unit
end
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 8d95dcee27..fc30690544 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -110,7 +110,13 @@ let make_coqtop_args fname =
| None -> args
| Some fname ->
if List.exists (String.equal "-top") args then args
- else "-topfile"::fname::args
+ else
+ (* We basically copy the code of Names.check_valid since it is not exported *)
+ (* to coqide. This is to prevent a possible failure of parsing "-topfile" *)
+ (* at initialization of coqtop (see #10286) *)
+ match Unicode.ident_refutation (Filename.chop_extension (Filename.basename fname)) with
+ | Some (_,x) -> output_string stderr (x^"\n"); exit 1
+ | None -> "-topfile"::fname::args
in
proj, args
@@ -160,7 +166,7 @@ let load_file ?(maycreate=false) f =
| [] -> false
| sn :: sessions ->
match sn.fileops#filename with
- | Some fn when is_f fn -> notebook#goto_page i; true
+ | Some fn when is_f fn -> notebook#goto_page i; true
| _ -> search_f (i+1) sessions
in
if not (search_f 0 notebook#pages) then begin
@@ -251,7 +257,7 @@ let crash_save exitcode =
in
try
if try_export filename (sn.buffer#get_text ()) then
- Minilib.log ("Saved "^filename)
+ Minilib.log ("Saved "^filename)
else Minilib.log ("Could not save "^filename)
with _ -> Minilib.log ("Could not save "^filename)
in
@@ -455,8 +461,8 @@ let compile sn =
|Some f ->
let args = Coq.get_arguments sn.coqtop in
let cmd = cmd_coqc#get
- ^ " " ^ String.concat " " args
- ^ " " ^ (Filename.quote f) ^ " 2>&1"
+ ^ " " ^ String.concat " " args
+ ^ " " ^ (Filename.quote f) ^ " 2>&1"
in
let buf = Buffer.create 1024 in
sn.messages#default_route#set (Pp.str ("Running: "^cmd));
@@ -603,9 +609,6 @@ module Nav = struct
let join_document _ = send_to_coq (fun sn -> sn.coqops#join_document)
end
-let tactic_wizard_callback l _ =
- send_to_coq (fun sn -> sn.coqops#tactic_wizard l)
-
let printopts_callback opts v =
let b = v#get_active in
let () = List.iter (fun o -> Coq.PrintOpt.set o b) opts in
@@ -881,10 +884,20 @@ let no_under = Util.String.map (fun x -> if x = '_' then '-' else x)
let alpha_items menu_name item_name l =
let mk_item text =
let text' =
- let last = String.length text - 1 in
- if text.[last] = '.'
- then text ^"\n"
- else text ^" "
+ let len = String.length text in
+ let buf = Buffer.create (len + 1) in
+ let escaped = ref false in
+ String.iter (fun c ->
+ if !escaped then
+ let () = Buffer.add_char buf c in
+ escaped := false
+ else if c = '_' then escaped := true
+ else Buffer.add_char buf c
+ ) text;
+ if text.[len - 1] = '.'
+ then Buffer.add_char buf '\n'
+ else Buffer.add_char buf ' ';
+ Buffer.contents buf
in
let callback _ =
on_current_term (fun sn -> sn.buffer#insert_interactive text')
@@ -953,6 +966,8 @@ let build_ui () =
with _ -> ()
in
let _ = w#event#connect#delete ~callback:(fun _ -> File.quit ~parent:w (); true) in
+ let _ = w#misc#connect#size_allocate
+ ~callback:(fun rect -> window_size := (rect.Gtk.width, rect.Gtk.height)) in
let _ = set_drag w#drag in
let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in
@@ -1003,7 +1018,7 @@ let build_ui () =
menu edit_menu [
item "Edit" ~label:"_Edit";
- item "Undo" ~accel:"<Ctrl>u" ~stock:`UNDO
+ item "Undo" ~accel:"<Primary>u" ~stock:`UNDO
~callback:(cb_on_current_term (fun t -> t.script#undo ()));
item "Redo" ~stock:`REDO
~callback:(cb_on_current_term (fun t -> t.script#redo ()));
@@ -1022,10 +1037,10 @@ let build_ui () =
~callback:(cb_on_current_term (fun t -> t.finder#find_backward ()));
item "External editor" ~label:"External editor" ~stock:`EDIT
~callback:(External.editor ~parent:w);
- item "Preferences" ~accel:"<Ctrl>comma" ~stock:`PREFERENCES
+ item "Preferences" ~accel:"<Primary>comma" ~stock:`PREFERENCES
~callback:(fun _ ->
begin
- try Preferences.configure ~apply:refresh_notebook_pos w
+ try Preferences.configure ~apply:refresh_notebook_pos w
with e ->
flash_info ("Editing preferences failed (" ^ Printexc.to_string e ^ ")")
end;
@@ -1040,19 +1055,19 @@ let build_ui () =
item "Next tab" ~label:"_Next tab" ~accel:"<Alt>Right"
~stock:`GO_FORWARD
~callback:(fun _ -> notebook#next_page ());
- item "Zoom in" ~label:"_Zoom in" ~accel:("<Control>plus")
+ item "Zoom in" ~label:"_Zoom in" ~accel:("<Primary>plus")
~stock:`ZOOM_IN ~callback:(fun _ ->
let ft = Pango.Font.from_string text_font#get in
Pango.Font.set_size ft (Pango.Font.get_size ft + Pango.scale);
text_font#set (Pango.Font.to_string ft);
save_pref ());
- item "Zoom out" ~label:"_Zoom out" ~accel:("<Control>minus")
+ item "Zoom out" ~label:"_Zoom out" ~accel:("<Primary>minus")
~stock:`ZOOM_OUT ~callback:(fun _ ->
let ft = Pango.Font.from_string text_font#get in
Pango.Font.set_size ft (Pango.Font.get_size ft - Pango.scale);
text_font#set (Pango.Font.to_string ft);
save_pref ());
- item "Zoom fit" ~label:"_Zoom fit" ~accel:("<Control>0")
+ item "Zoom fit" ~label:"_Zoom fit" ~accel:("<Primary>0")
~stock:`ZOOM_FIT ~callback:(cb_on_current_term MiscMenu.zoom_fit);
toggle_item "Show Toolbar" ~label:"Show _Toolbar"
~active:(show_toolbar#get)
@@ -1106,25 +1121,8 @@ let build_ui () =
("Force", "_Force", `EXECUTE, Nav.join_document, "Fully check the document", "f");
] end;
- let tacitem s sc =
- item s ~label:("_"^s)
- ~accel:(modifier_for_tactics#get^sc)
- ~callback:(tactic_wizard_callback [s])
- in
menu tactics_menu [
- item "Try Tactics" ~label:"_Try Tactics";
- item "Wizard" ~label:"<Proof Wizard>" ~stock:`DIALOG_INFO
- ~tooltip:"Proof Wizard" ~accel:(modifier_for_tactics#get^"dollar")
- ~callback:(tactic_wizard_callback automatic_tactics#get);
- tacitem "auto" "a";
- tacitem "auto with *" "asterisk";
- tacitem "eauto" "e";
- tacitem "eauto with *" "ampersand";
- tacitem "intuition" "i";
- tacitem "omega" "o";
- tacitem "simpl" "s";
- tacitem "tauto" "p";
- tacitem "trivial" "v";
+ item "Tactics" ~label:"_Tactics";
];
alpha_items tactics_menu "Tactic" Coq_commands.tactics;
@@ -1251,7 +1249,6 @@ let build_ui () =
let () = refresh_notebook_pos () in
let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in
let () = lower_hbox#pack ~expand:true status#coerce in
- let () = push_info ("Ready"^ if microPG#get then ", [μPG]" else "") in
(* Location display *)
let l = GMisc.label
@@ -1376,7 +1373,7 @@ let read_coqide_args argv =
|"-coqtop-flags" :: flags :: args->
Coq.ideslave_coqtop_flags := Some flags;
filter_coqtop coqtop project_files bindings_files out args
- |arg::args when out = [] && Minilib.is_prefix_of "-psn_" arg ->
+ |arg::args when out = [] && CString.is_prefix "-psn_" arg ->
(* argument added by MacOS during .app launch *)
filter_coqtop coqtop project_files bindings_files out args
|arg::args -> filter_coqtop coqtop project_files bindings_files (arg::out) args
diff --git a/ide/coqide_main.ml b/ide/coqide_main.ml
index f2ce2e8bd9..1e04d269f6 100644
--- a/ide/coqide_main.ml
+++ b/ide/coqide_main.ml
@@ -49,11 +49,10 @@ let catch_gtk_messages () =
let () = catch_gtk_messages ()
let load_prefs () =
- try Preferences.load_pref ()
- with e -> Ideutils.flash_info
- ("Could not load preferences ("^Printexc.to_string e^").")
+ Preferences.load_pref ~warn:(fun ~delay -> Ideutils.flash_info ~delay)
let () =
+ Ideutils.push_info ("Ready"^ if Preferences.microPG#get then ", [μPG]" else "");
load_prefs ();
let argl = List.tl (Array.to_list Sys.argv) in
let argl = Coqide.read_coqide_args argl in
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index d4a339f4f5..f056af6703 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -7,14 +7,14 @@ let list_items menu li =
let tactic_item = function
|[] -> Buffer.create 1
|[s] -> let b = Buffer.create 16 in
- let () = Buffer.add_string b ("<menuitem action='"^menu^" "^(no_under s)^"' />\n") in
- b
+ let () = Buffer.add_string b ("<menuitem action='"^menu^" "^(no_under s)^"' />\n") in
+ b
|s::_ as l -> let b = Buffer.create 50 in
- let () = (Buffer.add_string b ("<menu action='"^menu^" "^(String.make 1 s.[0])^"'>\n")) in
- let () = (List.iter
- (fun x -> Buffer.add_string b ("<menuitem action='"^menu^" "^(no_under x)^"' />\n")) l) in
- let () = Buffer.add_string b"</menu>\n" in
- b in
+ let () = (Buffer.add_string b ("<menu action='"^menu^" "^(String.make 1 s.[0])^"'>\n")) in
+ let () = (List.iter
+ (fun x -> Buffer.add_string b ("<menuitem action='"^menu^" "^(no_under x)^"' />\n")) l) in
+ let () = Buffer.add_string b"</menu>\n" in
+ b in
let () = List.iter (fun b -> Buffer.add_buffer res_buf (tactic_item b)) li in
res_buf
@@ -100,18 +100,7 @@ let init () =
\n <menuitem action='Previous' />\
\n <menuitem action='Next' />\
\n </menu>\
-\n <menu action='Try Tactics'>\
-\n <menuitem action='auto' />\
-\n <menuitem action='auto with *' />\
-\n <menuitem action='eauto' />\
-\n <menuitem action='eauto with *' />\
-\n <menuitem action='intuition' />\
-\n <menuitem action='omega' />\
-\n <menuitem action='simpl' />\
-\n <menuitem action='tauto' />\
-\n <menuitem action='trivial' />\
-\n <menuitem action='Wizard' />\
-\n <separator />\
+\n <menu action='Tactics'>\
\n %s\
\n </menu>\
\n <menu action='Templates'>\
@@ -173,7 +162,6 @@ let init () =
\n <toolitem action='Interrupt' />\
\n <toolitem action='Previous' />\
\n <toolitem action='Next' />\
-\n <toolitem action='Wizard' />\
\n</toolbar>\
\n</ui>"
(if Coq_config.gtk_platform <> `QUARTZ then "<menuitem action='Quit' />" else "")
diff --git a/ide/document.ml b/ide/document.ml
index cee490861d..b8e8182ab2 100644
--- a/ide/document.ml
+++ b/ide/document.ml
@@ -64,7 +64,7 @@ let tip = function
| { stack = [] } -> raise Empty
| { stack = { state_id = Some id }::_ } -> id
| { stack = { state_id = None }::_ } -> invalid_arg "tip"
-
+
let tip_data = function
| { stack = [] } -> raise Empty
| { stack = { data }::_ } -> data
@@ -89,19 +89,19 @@ let focus d ~cond_top:c_start ~cond_bot:c_stop =
else aux (x::a,s,b) grab xs
| { state_id = Some id; data } as x :: xs ->
if c_stop id data then List.rev a, List.rev (x::s), xs
- else aux (a,x::s,b) grab xs
+ else aux (a,x::s,b) grab xs
| _ -> assert false in
let a, s, b = aux ([],[],[]) false d.stack in
d.stack <- s;
d.context <- Some (a, b)
-
+
let unfocus = function
| { context = None } -> invalid_arg "unfocus"
| { context = Some (a,b); stack } as d ->
assert(invariant stack);
d.context <- None;
d.stack <- a @ stack @ b
-
+
let focused { context } = context <> None
let to_lists = function
@@ -117,17 +117,17 @@ let find d f =
try List.find (flat f true) s with Not_found ->
List.find (flat f false) b
).data
-
+
let find_map d f =
let a, s, b = to_lists d in
- try CList.find_map (flat f false) a with Not_found ->
- try CList.find_map (flat f true) s with Not_found ->
+ try CList.find_map (flat f false) a with Not_found ->
+ try CList.find_map (flat f true) s with Not_found ->
CList.find_map (flat f false) b
-
+
let is_empty = function
| { stack = []; context = None } -> true
| _ -> false
-
+
let context d =
let top, _, bot = to_lists d in
let pair _ x y = try Option.get x, y with Option.IsNone -> assert false in
diff --git a/ide/document.mli b/ide/document.mli
index eea250bd50..c0cc848bd7 100644
--- a/ide/document.mli
+++ b/ide/document.mli
@@ -11,7 +11,7 @@
(* An 'a document is a structure to hold and manipulate list of sentences.
Sentences are equipped with an id = Stateid.t and can carry arbitrary
data ('a).
-
+
When added (push) to the document, a sentence has no id, it has
be manually assigned just afterward or the sentence has to be removed
(pop) before any other sentence can be pushed.
@@ -21,7 +21,7 @@
sentence in question, and it is simpler if the sentence is in the document.
Only the functions pop, find, fold_all and find_map can be called on a
document with a tip that has no id (and assign_tip_id of course).
-
+
The document can be focused (non recursively) to a zone. After that
some functions operate on the focused zone only. When unfocused the
context (the part of the document out of focus) is restored.
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml
index a84c161a84..8e6d9f75c7 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/gtk_parsing.ml
@@ -12,50 +12,45 @@ let underscore = Glib.Utf8.to_unichar "_" ~pos:(ref 0)
let prime = Glib.Utf8.to_unichar "'" ~pos:(ref 0)
let dot = Glib.Utf8.to_unichar "." ~pos:(ref 0)
-(* TODO: avoid num and prime at the head of a word *)
-let is_word_char c =
- Glib.Unichar.isalnum c || c = underscore || c = prime || c = dot
+let find_word_start (it:GText.iter) =
+ let rec aux it good =
+ if it#is_start then good
+ else
+ let it = it#backward_char in
+ let c = it#char in
+ if Glib.Unichar.isalpha c || c = underscore then aux it it
+ else if Glib.Unichar.isalnum c || c = prime || c = dot then aux it good
+ else good in
+ aux it it
+let find_word_end (it:GText.iter) =
+ let rec aux it good =
+ if it#is_end then good
+ else
+ let c = it#char in
+ let it = it#forward_char in
+ if Glib.Unichar.isalnum c || c = prime || c = underscore then aux it it
+ else if c = dot then aux it good
+ else good in
+ aux it it
let starts_word (it:GText.iter) =
- (it#is_start ||
- (let c = it#backward_char#char in
- not (is_word_char c)))
+ if it#is_start then true
+ else
+ let it = it#backward_char in
+ let c = it#char in
+ if Glib.Unichar.isalpha c || c = underscore then
+ it#equal (find_word_start it)
+ else false
let ends_word (it:GText.iter) =
- (it#is_end ||
- let c = it#forward_char#char in
- not (is_word_char c)
- )
-
-let find_word_start (it:GText.iter) =
- let rec step_to_start it =
- Minilib.log "Find word start";
- if not it#nocopy#backward_char then
- (Minilib.log "find_word_start: cannot backward"; it)
- else if is_word_char it#char
- then step_to_start it
- else begin
- ignore(it#nocopy#forward_char);
- Minilib.log ("Word start at: "^(string_of_int it#offset));
- it
- end
- in
- step_to_start it#copy
-
-let find_word_end (it:GText.iter) =
- let rec step_to_end (it:GText.iter) =
- Minilib.log "Find word end";
+ if it#is_end then true
+ else
let c = it#char in
- if c<>0 && is_word_char c then (
- ignore (it#nocopy#forward_char);
- step_to_end it
- ) else (
- Minilib.log ("Word end at: "^(string_of_int it#offset));
- it)
- in
- step_to_end it#copy
-
+ let it = it#forward_char in
+ if Glib.Unichar.isalnum c || c = prime || c = underscore then
+ it#equal (find_word_end it)
+ else false
let get_word_around (it:GText.iter) =
let start = find_word_start it in
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 7c6fa8951b..7e55eb4d13 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -56,7 +56,7 @@ let coqide_known_option table = List.mem table [
["Printing";"Unfocused"];
["Diffs"]]
-let is_known_option cmd = match Vernacprop.under_control cmd with
+let is_known_option cmd = match cmd with
| VernacSetOption (_, o, OptionSetTrue)
| VernacSetOption (_, o, OptionSetString _)
| VernacSetOption (_, o, OptionUnset) -> coqide_known_option o
@@ -64,7 +64,7 @@ let is_known_option cmd = match Vernacprop.under_control cmd with
(** Check whether a command is forbidden in the IDE *)
-let ide_cmd_checks ~last_valid ({ CAst.loc; _ } as cmd) =
+let ide_cmd_checks ~last_valid { CAst.loc; v } =
let user_error s =
try CErrors.user_err ?loc ~hdr:"IDE" (str s)
with e ->
@@ -72,14 +72,14 @@ let ide_cmd_checks ~last_valid ({ CAst.loc; _ } as cmd) =
let info = Stateid.add info ~valid:last_valid Stateid.dummy in
Exninfo.raise ~info e
in
- if is_debug cmd then
+ if is_debug v.expr then
user_error "Debug mode not available in the IDE"
-let ide_cmd_warns ~id ({ CAst.loc; _ } as cmd) =
+let ide_cmd_warns ~id { CAst.loc; v } =
let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in
- if is_known_option cmd then
+ if is_known_option v.expr then
warn "Set this option from the IDE menu instead";
- if is_navigation_vernac cmd || is_undo cmd then
+ if is_navigation_vernac v.expr || is_undo v.expr then
warn "Use IDE navigation instead"
(** Interpretation (cf. [Ide_intf.interp]) *)
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 246254c6a5..1cf065cf25 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -18,8 +18,8 @@ let warn_image () =
img#set_icon_size `DIALOG;
img
-let warning msg =
- GToolbox.message_box ~title:"Warning" ~icon:(warn_image ())#coerce msg
+let warning msg =
+ GToolbox.message_box ~title:"Warning" ~icon:(warn_image ())#coerce msg
let cb = GData.clipboard Gdk.Atom.primary
@@ -34,9 +34,38 @@ let push_info,pop_info,clear_info =
(fun () -> decr size; status_context#pop ()),
(fun () -> for _i = 1 to !size do status_context#pop () done; size := 0)
+type 'a mlist = Nil | Cons of { hd : 'a ; mutable tl : 'a mlist }
+
+let enqueue a x =
+ let rec aux x = match x with
+ | Nil -> assert false
+ | Cons p ->
+ match p.tl with
+ | Nil -> p.tl <- Cons { hd = a ; tl = Nil }
+ | _ -> aux p.tl in
+ match !x with
+ | Nil -> x := Cons { hd = a ; tl = Nil }
+ | _ -> aux !x
+
+let pop = function
+ | Cons p -> p.tl
+ | Nil -> assert false
+
let flash_info =
+ let queue = ref Nil in
let flash_context = status#new_context ~name:"Flash" in
- (fun ?(delay=5000) s -> flash_context#flash ~delay s)
+ let rec process () = match !queue with
+ | Cons { hd = (delay,text) } ->
+ let msg = flash_context#push text in
+ ignore (Glib.Timeout.add ~ms:delay ~callback:(fun () ->
+ flash_context#remove msg;
+ queue := pop !queue;
+ process (); false))
+ | Nil -> () in
+ fun ?(delay=5000) text ->
+ let processing = !queue <> Nil in
+ enqueue (delay,text) queue;
+ if not processing then process ()
(* Note: Setting the same attribute with two separate tags appears to use
the first value applied and not the second. I saw this trying to set the background
@@ -183,15 +212,15 @@ let try_export file_name s =
try match encoding#get with
|Eutf8 -> Minilib.log "UTF-8 is enforced" ; s
|Elocale ->
- let is_unicode,char_set = Glib.Convert.get_charset () in
- if is_unicode then
- (Minilib.log "Locale is UTF-8" ; s)
- else
- (Minilib.log ("Locale is "^char_set);
- Glib.Convert.convert_with_fallback
+ let is_unicode,char_set = Glib.Convert.get_charset () in
+ if is_unicode then
+ (Minilib.log "Locale is UTF-8" ; s)
+ else
+ (Minilib.log ("Locale is "^char_set);
+ Glib.Convert.convert_with_fallback
~from_codeset:"UTF-8" ~to_codeset:char_set s)
|Emanual enc ->
- (Minilib.log ("Manual charset is "^ enc);
+ (Minilib.log ("Manual charset is "^ enc);
Glib.Convert.convert_with_fallback
~from_codeset:"UTF-8" ~to_codeset:enc s)
with e ->
@@ -250,9 +279,9 @@ let select_file_for_open ~title ?(filter=true) ?parent ?filename () =
match file_chooser#run () with
| `OPEN ->
begin
- match file_chooser#filename with
- | None -> None
- | Some _ as f ->
+ match file_chooser#filename with
+ | None -> None
+ | Some _ as f ->
project_path#set file_chooser#current_folder; f
end
| `DELETE_EVENT | `CANCEL -> None in
@@ -336,12 +365,12 @@ let coqtop_path () =
if Sys.file_exists new_prog ||
CString.equal Filename.(basename new_prog) new_prog
then new_prog
- else
- let in_macos_bundle =
- Filename.concat
- (Filename.dirname new_prog)
- (Filename.concat "../Resources/bin" (Filename.basename new_prog))
- in if Sys.file_exists in_macos_bundle then in_macos_bundle
+ else
+ let in_macos_bundle =
+ Filename.concat
+ (Filename.dirname new_prog)
+ (Filename.concat "../Resources/bin" (Filename.basename new_prog))
+ in if Sys.file_exists in_macos_bundle then in_macos_bundle
else "coqidetop.opt"
with Not_found -> "coqidetop.opt"
in file
diff --git a/ide/microPG.ml b/ide/microPG.ml
index 7d8fd44a75..9492f1a77f 100644
--- a/ide/microPG.ml
+++ b/ide/microPG.ml
@@ -153,7 +153,7 @@ let run key gui action status =
else (b#place_cursor ~where; script#scroll_mark_onscreen `INSERT);
status
-let emacs = empty
+let emacs = empty
let emacs = insert emacs "Emacs" [] [
(* motion *)
@@ -214,7 +214,7 @@ let emacs = insert emacs "Emacs" [] [
let k =
if i#ends_line then begin
b#delete ~start:i ~stop:i#forward_char; "\n"
- end else begin
+ end else begin
let k = b#get_text ~start:i ~stop:i#forward_to_line_end () in
b#delete ~start:i ~stop:i#forward_to_line_end; k
end in
@@ -265,7 +265,7 @@ let emacs = insert emacs "Emacs" [mC,_x,"x"] [
mkE _f "f" "Open" (Action("File", "Open"));
mkE ~mods:[] _u "u" "Undo" (Action("Edit", "Undo"));
]
-
+
let pg = insert emacs "Proof General" [mC,_c,"c"] [
mkE _Return "RET" "Go to" (Action("Navigation", "Go to"));
mkE _n "n" "Advance 1 sentence" (Action("Navigation", "Forward"));
diff --git a/ide/minilib.ml b/ide/minilib.ml
index 09a7112098..926ad27abc 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -58,17 +58,13 @@ let coqide_data_dirs () =
:: List.map coqify (Glib.get_system_data_dirs ())
@ [Envars.datadir ()]
-let coqide_config_dirs () =
- coqide_config_home ()
- :: List.map coqify (Glib.get_system_config_dirs ())
- @ [Envars.configdir ()]
+let coqide_system_config_dirs () =
+ List.map coqify (Glib.get_system_config_dirs ())
-let is_prefix_of pre s =
- let i = ref 0 in
- let () = while (!i < (String.length pre)
- && !i < (String.length s)
- && pre.[!i] = s.[!i]) do
- incr i
- done
- in !i = String.length pre
+let coqide_default_config_dir () =
+ Envars.configdir ()
+let coqide_config_dirs () =
+ coqide_config_home () ::
+ coqide_system_config_dirs () @
+ [coqide_default_config_dir ()]
diff --git a/ide/minilib.mli b/ide/minilib.mli
index c5849cc2c9..a9d26ee7d2 100644
--- a/ide/minilib.mli
+++ b/ide/minilib.mli
@@ -27,7 +27,19 @@ val debug : bool ref
val log_pp : ?level:level -> Pp.t -> unit
val log : ?level:level -> string -> unit
+(* The directory where user config files are conventionally *)
+(* installed on the current platform (as given by Glib) *)
val coqide_config_home : unit -> string
+
+(* The directories where system-wide config files are conventionally *)
+(* installed on the current platform (as given by Glib) *)
+val coqide_system_config_dirs : unit -> string list
+
+(* The directory where default config files are installed at installation time *)
+val coqide_default_config_dir : unit -> string
+
+(* The ordered list of directories where a config file is searched by default *)
val coqide_config_dirs : unit -> string list
+
+(* The ordered list of directories where a data file is searched by default *)
val coqide_data_dirs : unit -> string list
-val is_prefix_of : string -> string -> bool
diff --git a/ide/preferences.ml b/ide/preferences.ml
index ea0495bb19..4ee5669877 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -10,8 +10,6 @@
open Configwin
-let pref_file = Filename.concat (Minilib.coqide_config_home ()) "coqiderc"
-let accel_file = Filename.concat (Minilib.coqide_config_home ()) "coqide.keys"
let lang_manager = GSourceView3.source_language_manager ~default:true
let () = lang_manager#set_search_path
((Minilib.coqide_data_dirs ())@lang_manager#search_path)
@@ -235,22 +233,13 @@ end
end
-let get_config_file name =
+let get_config_file dirs name =
let find_config dir = Sys.file_exists (Filename.concat dir name) in
- let config_dir = List.find find_config (Minilib.coqide_config_dirs ()) in
+ let config_dir = List.find find_config dirs in
Filename.concat config_dir name
-(* Small hack to handle v8.3 to v8.4 change in configuration file *)
-let loaded_pref_file =
- try get_config_file "coqiderc"
- with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqiderc"
-
-let loaded_accel_file =
- try get_config_file "coqide.keys"
- with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqide.keys"
-
let get_unicode_bindings_local_file () =
- try Some (get_config_file "coqide.bindings")
+ try Some (get_config_file [Minilib.coqide_config_home ()] "coqide.bindings")
with Not_found -> None
let get_unicode_bindings_default_file () =
@@ -332,26 +321,36 @@ let attach_modifiers (pref : string preference) prefix =
in
pref#connect#changed ~callback:cb
+let select_arch m m_osx =
+ if Coq_config.arch = "Darwin" then m_osx else m
+
let modifier_for_navigation =
- new preference ~name:["modifier_for_navigation"] ~init:"<Control>" ~repr:Repr.(string)
+ new preference ~name:["modifier_for_navigation"]
+ ~init:(select_arch "<Control>" "<Control><Primary>") ~repr:Repr.(string)
let modifier_for_templates =
new preference ~name:["modifier_for_templates"] ~init:"<Control><Shift>" ~repr:Repr.(string)
let modifier_for_tactics =
- new preference ~name:["modifier_for_tactics"] ~init:"<Control><Alt>" ~repr:Repr.(string)
+ new preference ~name:["modifier_for_tactics"]
+ ~init:(select_arch "<Control><Alt>" "<Control><Primary>") ~repr:Repr.(string)
let modifier_for_display =
- new preference ~name:["modifier_for_display"] ~init:"<Alt><Shift>" ~repr:Repr.(string)
+ new preference ~name:["modifier_for_display"]
+ ~init:(select_arch "<Alt><Shift>" "<Primary><Shift>")~repr:Repr.(string)
let modifier_for_queries =
new preference ~name:["modifier_for_queries"] ~init:"<Control><Shift>" ~repr:Repr.(string)
-let _ = attach_modifiers modifier_for_navigation "<Actions>/Navigation/"
-let _ = attach_modifiers modifier_for_templates "<Actions>/Templates/"
-let _ = attach_modifiers modifier_for_tactics "<Actions>/Tactics/"
-let _ = attach_modifiers modifier_for_display "<Actions>/View/"
-let _ = attach_modifiers modifier_for_queries "<Actions>/Queries/"
+let attach_modifiers_callback () =
+ (* Tell to propagate changes done in preference menu to accel map *)
+ (* To be done after the preferences are loaded *)
+ let _ = attach_modifiers modifier_for_navigation "<Actions>/Navigation/" in
+ let _ = attach_modifiers modifier_for_templates "<Actions>/Templates/" in
+ let _ = attach_modifiers modifier_for_tactics "<Actions>/Tactics/" in
+ let _ = attach_modifiers modifier_for_display "<Actions>/View/" in
+ let _ = attach_modifiers modifier_for_queries "<Actions>/Queries/" in
+ ()
let modifiers_valid =
new preference ~name:["modifiers_valid"] ~init:"<Alt><Control><Shift>" ~repr:Repr.(string)
@@ -380,9 +379,6 @@ let text_font =
let show_toolbar =
new preference ~name:["show_toolbar"] ~init:true ~repr:Repr.(bool)
-let contextual_menus_on_goal =
- new preference ~name:["contextual_menus_on_goal"] ~init:true ~repr:Repr.(bool)
-
let window_width =
new preference ~name:["window_width"] ~init:800 ~repr:Repr.(int)
@@ -644,29 +640,73 @@ let tag_button () =
let box = GPack.hbox () in
new tag_button (Gobject.unsafe_cast box#as_widget)
-let save_pref () =
+(** Loading/saving preferences *)
+
+let pref_file = Filename.concat (Minilib.coqide_config_home ()) "coqiderc"
+let accel_file = Filename.concat (Minilib.coqide_config_home ()) "coqide.keys"
+
+let save_accel_pref () =
+ if not (Sys.file_exists (Minilib.coqide_config_home ()))
+ then Unix.mkdir (Minilib.coqide_config_home ()) 0o700;
+ GtkData.AccelMap.save accel_file
+
+let save_rc_pref () =
if not (Sys.file_exists (Minilib.coqide_config_home ()))
then Unix.mkdir (Minilib.coqide_config_home ()) 0o700;
- let () = try GtkData.AccelMap.save accel_file with _ -> () in
let add = Util.String.Map.add in
let fold key obj accu = add key (obj.get ()) accu in
let prefs = Util.String.Map.fold fold !preferences Util.String.Map.empty in
let prefs = Util.String.Map.fold Util.String.Map.add !unknown_preferences prefs in
Config_lexer.print_file pref_file prefs
-let load_pref () =
- (* Load main preference file *)
- let () =
- let m = Config_lexer.load_file loaded_pref_file in
+let save_pref () =
+ save_accel_pref ();
+ save_rc_pref ()
+
+let try_load_pref_file loader warn file =
+ try
+ loader file
+ with
+ e -> warn ~delay:5000 ("Could not load " ^ file ^ " ("^Printexc.to_string e^")")
+
+let load_pref_file loader warn name =
+ try
+ let user_file = get_config_file [Minilib.coqide_config_home ()] name in
+ warn ~delay:2000 ("Loading " ^ user_file);
+ try_load_pref_file loader warn user_file
+ with Not_found ->
+ try
+ let system_wide_file = get_config_file (Minilib.coqide_system_config_dirs ()) name in
+ warn ~delay:5000 ("No user " ^ name ^ ", using system wide configuration");
+ try_load_pref_file loader warn system_wide_file
+ with Not_found ->
+ (* Compatibility with oldest versions of CoqIDE (<= 8.4) *)
+ try
+ let old_user_file = get_config_file [Option.default "" (Glib.get_home_dir ())] ("."^name) in
+ warn ~delay:5000 ("No " ^ name ^ ", trying to recover from an older version of CoqIDE");
+ try_load_pref_file loader warn old_user_file
+ with Not_found ->
+ (* Built-in configuration *)
+ warn ~delay:5000 ("No " ^ name ^ ", using default internal configuration")
+
+let load_accel_pref ~warn =
+ load_pref_file GtkData.AccelMap.load warn "coqide.keys"
+
+let load_rc_pref ~warn =
+ let loader file =
+ let m = Config_lexer.load_file file in
let iter name v =
if Util.String.Map.mem name !preferences then
try (Util.String.Map.find name !preferences).set v with _ -> ()
else unknown_preferences := Util.String.Map.add name v !unknown_preferences
in
Util.String.Map.iter iter m in
- (* Load file for bindings *)
- let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in
- ()
+ load_pref_file loader warn "coqiderc";
+ attach_modifiers_callback ()
+
+let load_pref ~warn =
+ load_rc_pref ~warn;
+ load_accel_pref ~warn
let pstring name p = string ~f:p#set name p#get
let pbool name p = bool ~f:p#set name p#get
@@ -695,13 +735,13 @@ let configure ?(apply=(fun () -> ())) parent =
"Goal (∃n : nat, n ≤ 0)∧(∀x,y,z, x∈y⋃z↔x∈y∨x∈z).";
box#pack ~expand:true w#coerce;
ignore (w#misc#connect#realize
- ~callback:(fun () -> w#set_font_name text_font#get));
+ ~callback:(fun () -> w#set_font_name text_font#get));
custom
~label:"Fonts for text"
box
(fun () ->
- let fd = w#font_name in
- text_font#set fd)
+ let fd = w#font_name in
+ text_font#set fd)
true
in
@@ -823,7 +863,7 @@ let configure ?(apply=(fun () -> ())) parent =
let global_auto_revert_delay =
string
~f:(fun s -> global_auto_revert_delay#set
- (try int_of_string s with _ -> 10000))
+ (try int_of_string s with _ -> 10000))
"Global auto revert delay (ms)"
(string_of_int global_auto_revert_delay#get)
in
@@ -832,7 +872,7 @@ let configure ?(apply=(fun () -> ())) parent =
let auto_save_delay =
string
~f:(fun s -> auto_save_delay#set
- (try int_of_string s with _ -> 10000))
+ (try int_of_string s with _ -> 10000))
"Auto save delay (ms)"
(string_of_int auto_save_delay#get)
in
@@ -851,8 +891,8 @@ let configure ?(apply=(fun () -> ())) parent =
~f:(fun s -> encoding#set (inputenc_of_string s))
~new_allowed: true
("UTF-8"::"LOCALE":: match encoding#get with
- |Emanual s -> [s]
- |_ -> []
+ |Emanual s -> [s]
+ |_ -> []
)
(string_of_inputenc encoding#get)
in
@@ -893,19 +933,19 @@ let configure ?(apply=(fun () -> ())) parent =
in
let project_file_name = pstring "Default name for project file" project_file_name in
let modifier_for_tactics =
- pmodifiers "Modifiers for Tactics Menu" modifier_for_tactics
+ pmodifiers "Global change of modifiers for Tactics Menu" modifier_for_tactics
in
let modifier_for_templates =
- pmodifiers "Modifiers for Templates Menu" modifier_for_templates
+ pmodifiers "Global change of modifiers for Templates Menu" modifier_for_templates
in
let modifier_for_navigation =
- pmodifiers "Modifiers for Navigation Menu" modifier_for_navigation
+ pmodifiers "Global change of modifiers for Navigation Menu" modifier_for_navigation
in
let modifier_for_display =
- pmodifiers "Modifiers for View Menu" modifier_for_display
+ pmodifiers "Global change of modifiers for View Menu" modifier_for_display
in
let modifier_for_queries =
- pmodifiers "Modifiers for Queries Menu" modifier_for_queries
+ pmodifiers "Global change of modifiers for Queries Menu" modifier_for_queries
in
let modifiers_valid =
pmodifiers ~all:true "Allowed modifiers" modifiers_valid
@@ -938,20 +978,8 @@ let configure ?(apply=(fun () -> ())) parent =
else cmd_browse#get])
cmd_browse#get
in
-(*
- let automatic_tactics =
- strings
- ~f:automatic_tactics#set
- ~add:(fun () -> ["<edit me>"])
- "Wizard tactics to try in order"
- automatic_tactics#get
-
- in
-*)
- let contextual_menus_on_goal = pbool "Contextual menus on goal" contextual_menus_on_goal in
-
- let misc = [contextual_menus_on_goal;stop_before;reset_on_tab_switch;
+ let misc = [stop_before;reset_on_tab_switch;
vertical_tabs;opposite_tabs] in
(*
@@ -990,30 +1018,26 @@ let configure ?(apply=(fun () -> ())) parent =
(shame on Benjamin) *)
let cmds =
[Section("Fonts", Some `SELECT_FONT,
- [config_font]);
+ [config_font]);
Section("Colors", Some `SELECT_COLOR,
[config_color; source_language; source_style]);
Section("Tags", Some `SELECT_COLOR,
[config_tags]);
Section("Editor", Some `EDIT, [config_editor]);
Section("Files", Some `DIRECTORY,
- [global_auto_revert;global_auto_revert_delay;
- auto_save; auto_save_delay; (* auto_save_name*)
- encodings; line_ending;
- ]);
+ [global_auto_revert;global_auto_revert_delay;
+ auto_save; auto_save_delay; (* auto_save_name*)
+ encodings; line_ending;
+ ]);
Section("Project", Some (`STOCK "gtk-page-setup"),
- [project_file_name;read_project;
- ]);
+ [project_file_name;read_project;
+ ]);
Section("Appearance", Some `PREFERENCES, [window_width; window_height]);
Section("Externals", None,
- [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc;
+ [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc;
cmd_print;cmd_editor;cmd_browse]);
-(*
- Section("Tactics Wizard", None,
- [automatic_tactics]);
-*)
Section("Shortcuts", Some `PREFERENCES,
- [modifiers_valid; modifier_for_tactics;
+ [modifiers_valid; modifier_for_tactics;
modifier_for_templates; modifier_for_display; modifier_for_navigation;
modifier_for_queries (*; user_queries *)]);
Section("Misc", Some `ADD,
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 490756d4f2..4b04326cec 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -79,7 +79,6 @@ val cmd_browse : string preference
val cmd_editor : string preference
val text_font : string preference
val show_toolbar : bool preference
-val contextual_menus_on_goal : bool preference
val window_width : int preference
val window_height : int preference
val auto_complete : bool preference
@@ -107,7 +106,7 @@ val user_queries : (string * string) list preference
val diffs : string preference
val save_pref : unit -> unit
-val load_pref : unit -> unit
+val load_pref : warn:(delay:int -> string -> unit) -> unit
val configure : ?apply:(unit -> unit) -> GWindow.window -> unit
diff --git a/ide/protocol/xml_lexer.mli b/ide/protocol/xml_lexer.mli
index e61cb055f7..920de9f9c3 100644
--- a/ide/protocol/xml_lexer.mli
+++ b/ide/protocol/xml_lexer.mli
@@ -18,26 +18,26 @@
*)
type error =
- | EUnterminatedComment
- | EUnterminatedString
- | EIdentExpected
- | ECloseExpected
- | ENodeExpected
- | EAttributeNameExpected
- | EAttributeValueExpected
- | EUnterminatedEntity
+ | EUnterminatedComment
+ | EUnterminatedString
+ | EIdentExpected
+ | ECloseExpected
+ | ENodeExpected
+ | EAttributeNameExpected
+ | EAttributeValueExpected
+ | EUnterminatedEntity
exception Error of error
type token =
- | Tag of string * (string * string) list * bool
- | PCData of string
- | Endtag of string
- | Eof
+ | Tag of string * (string * string) list * bool
+ | PCData of string
+ | Endtag of string
+ | Eof
type pos = int * int * int * int
-val init : Lexing.lexbuf -> unit
+val init : Lexing.lexbuf -> unit
val close : unit -> unit
val token : Lexing.lexbuf -> token
val pos : Lexing.lexbuf -> pos
diff --git a/ide/session.ml b/ide/session.ml
index a9c106a765..547c9814ff 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -149,7 +149,7 @@ let set_buffer_handlers
let rec aux old it =
if it#is_start then None
else if it#has_tag Tags.Script.processed then Some old
- else if it#has_tag Tags.Script.error_bg then aux it it#backward_char
+ else if it#has_tag Tags.Script.error_bg then aux it it#backward_char
else None in
aux it it in
let insert_cb it s = if String.length s = 0 then () else begin
@@ -207,8 +207,8 @@ let set_buffer_handlers
to a point indicated by coq. *)
if !no_coq_action_required then begin
let start, stop = get_start (), get_stop () in
- List.iter (fun tag -> buffer#remove_tag tag ~start ~stop)
- Tags.Script.ephemere;
+ List.iter (fun tag -> buffer#remove_tag tag ~start ~stop)
+ Tags.Script.ephemere;
Sentence.tag_on_insert buffer
end;
end in
@@ -301,7 +301,7 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
script#buffer#place_cursor ~where;
script#misc#grab_focus ();
ignore (script#scroll_to_iter
- ~use_align:false ~yalign:0.75 ~within_margin:0.25 where)) in
+ ~use_align:false ~yalign:0.75 ~within_margin:0.25 where)) in
let tip = GMisc.label ~text:"Double click to jump to error line" () in
let box = GPack.vbox ~homogeneous:false () in
let () = box#pack ~expand:true table#coerce in
@@ -313,10 +313,10 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
method update errs =
if !last_update = errs then ()
else begin
- last_update := errs;
- access (fun _ store -> store#clear ());
+ last_update := errs;
+ access (fun _ store -> store#clear ());
!callback errs;
- List.iter (fun (lno, msg) -> access (fun columns store ->
+ List.iter (fun (lno, msg) -> access (fun columns store ->
let line = store#append () in
store#set ~row:line ~column:(find_int_col "Line" columns) lno;
store#set ~row:line ~column:(find_string_col "Error message" columns) msg))
@@ -333,8 +333,8 @@ let create_jobpage coqtop coqops : jobpage =
(fun columns store tp vc ->
let row = store#get_iter tp in
let w = store#get ~row ~column:(find_string_col "Worker" columns) in
- let info () = Minilib.log ("Coq busy, discarding query") in
- Coq.try_grab coqtop (coqops#stop_worker w) info
+ let info () = Minilib.log ("Coq busy, discarding query") in
+ Coq.try_grab coqtop (coqops#stop_worker w) info
) in
let tip = GMisc.label ~text:"Double click to interrupt worker" () in
let box = GPack.vbox ~homogeneous:false () in
@@ -347,10 +347,10 @@ let create_jobpage coqtop coqops : jobpage =
method update jobs =
if !last_update = jobs then ()
else begin
- last_update := jobs;
- access (fun _ store -> store#clear ());
+ last_update := jobs;
+ access (fun _ store -> store#clear ());
!callback jobs;
- CString.Map.iter (fun id job -> access (fun columns store ->
+ CString.Map.iter (fun id job -> access (fun columns store ->
let column = find_string_col "Worker" columns in
if job = "Dead" then
store#foreach (fun _ row ->
@@ -432,6 +432,8 @@ let kill (sn:session) =
sn.script#destroy ();
Coq.close_coqtop sn.coqtop
+let window_size = ref (window_width#get, window_height#get)
+
let build_layout (sn:session) =
let session_paned = GPack.paned `VERTICAL () in
let session_box =
@@ -502,19 +504,25 @@ let build_layout (sn:session) =
~callback:(fun () -> if sn.buffer#modified
then img#set_stock `SAVE
else img#set_stock `YES) in
- let _ =
- eval_paned#misc#connect#size_allocate
- ~callback:
- (let b = ref true in
- fun {Gtk.width=paned_width;Gtk.height=paned_height} ->
- if !b then begin
- eval_paned#set_position
- (paned_width / 2);
- state_paned#set_position
- (paned_height / 2);
- b := false
- end)
- in
+ (* There was an issue in the previous implementation for setting the
+ position of the handle. It was using the size_allocate event but
+ there is an issue with size_allocate. G. Melquiond analyzed that
+ at starting time, the size_allocate event is only issued in
+ Layout phase of the gtk loop so that it is actually processed
+ only in the next iteration of the event-update-layout-paint loop,
+ after the user does something and trigger an effective new event
+ (see #10578). So we preventively enforce an estimated position
+ for the handles to be used in the very first initializing
+ iteration of the loop *)
+ let () =
+ (* 14 is the estimated size for vertical borders *)
+ let estimated_vertical_handle_position = (fst !window_size - 14) / 2 in
+ (* 169 is the estimated size for menus, command line, horizontal border *)
+ let estimated_horizontal_handle_position = (snd !window_size - 169) / 2 in
+ if estimated_vertical_handle_position > 0 then
+ eval_paned#set_position estimated_vertical_handle_position;
+ if estimated_horizontal_handle_position > 0 then
+ state_paned#set_position estimated_horizontal_handle_position in
session_box#pack sn.finder#coerce;
session_box#pack sn.segment#coerce;
sn.command#pack_in (session_paned#pack2 ~shrink:false ~resize:false);
@@ -538,8 +546,6 @@ let build_layout (sn:session) =
else (label#set_text (red txt);label#set_use_markup true));
session_tab#pack sn.tab_label#coerce;
img#set_stock `YES;
- eval_paned#set_position 1;
- state_paned#set_position 1;
let control =
object
method detach () = proof_detachable#detach ()
diff --git a/ide/session.mli b/ide/session.mli
index f5d8d7c991..63ac1e6dc0 100644
--- a/ide/session.mli
+++ b/ide/session.mli
@@ -51,3 +51,5 @@ val kill : session -> unit
val build_layout : session ->
GObj.widget option * GObj.widget option * GObj.widget
+
+val window_size : (int * int) ref
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index f1a2fa4f2a..dcae3e38a5 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -93,9 +93,9 @@ object(self)
combo, entry, ok_b in
let r_bin =
GBin.scrolled_window
- ~vpolicy:`AUTOMATIC
- ~hpolicy:`AUTOMATIC
- ~packing:(vbox#pack ~fill:true ~expand:true) () in
+ ~vpolicy:`AUTOMATIC
+ ~hpolicy:`AUTOMATIC
+ ~packing:(vbox#pack ~fill:true ~expand:true) () in
let result = Wg_MessageView.message_view () in
router#register_route route_id result;
r_bin#add_with_viewport (result :> GObj.widget);
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml
index 98390e810f..ac6712909e 100644
--- a/ide/wg_Completion.ml
+++ b/ide/wg_Completion.ml
@@ -175,7 +175,7 @@ object (self)
let log = Printf.sprintf "Completion at offset: %i" insert_offset in
let () = Minilib.log log in
let prefix =
- if Gtk_parsing.ends_word iter#backward_char then
+ if Gtk_parsing.ends_word iter then
let start = Gtk_parsing.find_word_start iter in
let w = buffer#get_text ~start ~stop:iter () in
if String.length w >= auto_complete_length then Some (w, start)
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index db99bc0439..c0ece1ecdc 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -11,9 +11,9 @@
let b2c = Ideutils.byte_offset_to_char_offset
class finder name (view : GText.view) =
-
+
let widget = Wg_Detachable.detachable
- ~title:(Printf.sprintf "Find & Replace (%s)" name) () in
+ ~title:(Printf.sprintf "Find & Replace (%s)" name) () in
let replace_box = GPack.grid (* ~columns:4 ~rows:2 *) ~col_homogeneous:false ~row_homogeneous:false
~packing:widget#add () in
let hb = GPack.hbox ~packing:(replace_box#attach
@@ -75,7 +75,7 @@ class finder name (view : GText.view) =
if use_regex#active then
if use_nocase#active then Str.regexp_case_fold rex
else Str.regexp rex
- else
+ else
if use_nocase#active then Str.regexp_string_case_fold rex
else Str.regexp_string rex
@@ -94,7 +94,7 @@ class finder name (view : GText.view) =
Some(view#buffer#start_iter#forward_chars (b2c text i),
view#buffer#start_iter#forward_chars (b2c text j))
with Not_found -> None
-
+
method private forward_search starti =
let text = starti#get_text ~stop:view#buffer#end_iter in
let regexp = self#regex in
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 279815d671..769ce61ee1 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -408,10 +408,8 @@ object (self)
| _ -> ()
method apply_unicode_binding () =
- (* Auxiliary method to reach the beginning of line or the
- nearest space before the iterator. *)
let rec get_line_start iter =
- if iter#starts_line || Glib.Unichar.isspace iter#char then iter
+ if iter#starts_line then iter
else get_line_start iter#backward_char
in
(* Main action *)
@@ -496,10 +494,10 @@ object (self)
let proceed =
if not b && i = 1 then
iter#editable ~default:true &&
- iter#forward_line#editable ~default:true
+ iter#forward_line#editable ~default:true
else if not b && i = -1 then
iter#editable ~default:true &&
- iter#backward_line#editable ~default:true
+ iter#backward_line#editable ~default:true
else false
in
if not proceed then GtkSignal.stop_emit ()
@@ -541,13 +539,13 @@ let script_view ct ?(source_buffer:GSourceView3.source_buffer option) ?draw_spa
GtkSourceView3.SourceView.make_params [] ~cont:(
GtkText.View.make_params ~cont:(
GContainer.pack_container ~create:
- (fun pl ->
- let w = match source_buffer with
+ (fun pl ->
+ let w = match source_buffer with
| None -> GtkSourceView3.SourceView.new_ ()
| Some buf -> GtkSourceView3.SourceView.new_with_buffer
(Gobject.try_cast buf#as_buffer "GtkSourceBuffer")
- in
- let w = Gobject.unsafe_cast w in
- Gobject.set_params (Gobject.try_cast w "GtkSourceView") pl;
+ in
+ let w = Gobject.unsafe_cast w in
+ Gobject.set_params (Gobject.try_cast w "GtkSourceView") pl;
Gaux.may ~f:(GtkSourceView3.SourceView.set_draw_spaces w) draw_spaces;
- ((new script_view w ct) : script_view))))
+ ((new script_view w ct) : script_view))))
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 04:19:59 +0000