Changeset 141:45729175615f

Timestamp:

08/01/2008 03:00:20 PM (4 months ago)

Author:

marc@f1.local

branch:

default

Message:

fix for #88

Files:

• development/java/field/core/DragDuplicator.java (modified) (2 diffs)
• development/java/field/core/StandardFluidSheet.java (modified) (1 diff)
• development/java/field/core/ui/text/BaseTextEditor2.java (modified) (3 diffs)
• development/java/field/core/ui/text/PythonTextEditor.java (modified) (1 diff)

development/java/field/core/DragDuplicator.java

@@ -43 +43 @@
-        public void begin(MouseEvent event) {
-
-                NSCursor.closedHandCursor().set();
-
-                Set<iComponent> c = group.getSelection();
@@ -56 +55 @@
-
-                if (isDragging) {
+                        NSCursor.closedHandCursor().set();
-                        FluidCopyPastePersistence copier = iVisualElement.copyPaste.get(root);
-

development/java/field/core/StandardFluidSheet.java

@@ -754 +754 @@
-                        }
-                }
+
+                List<String> w = pp.getWarnings();
+                if (w.size()>0)
+                {
+                        System.err.println(" warning while saving :"+w);
+                }
+
-                return pp.getWarnings();
-

development/java/field/core/ui/text/BaseTextEditor2.java

@@ -1006 +1006 @@
-                                DefaultStyledDocument doc = (DefaultStyledDocument) ed.getDocument();
-                                Element element = doc.getCharacterElement(offset);
-//
+
-
-                                if (element.getName().toLowerCase().equals("component")) {
-//
+
-                                } else
-                                        fb.insertString(offset, string, attr);
@@ -1018 +1018 @@
-                                DefaultStyledDocument doc = (DefaultStyledDocument) ed.getDocument();
-                                Element element = doc.getCharacterElement(offset);
-//
+
-                                if (element.getName().toLowerCase().equals("component")) {
-//
+
-                                } else
-                                        fb.replace(offset, length, text, attrs);
@@ -1029 +1029 @@
-                                DefaultStyledDocument doc = (DefaultStyledDocument) ed.getDocument();
-                                Element element = doc.getCharacterElement(offset);
-//
+
-                                if (element.getName().toLowerCase().equals("component")) {
-//
+
-                                        fb.remove(element.getStartOffset(), element.getEndOffset() - element.getStartOffset());
-                                } else

development/java/field/core/ui/text/PythonTextEditor.java

@@ -508 +508 @@
-
-        public void setText(String string) {
+                System.out.println(" about to set text to nothing ");
+
+                ed.setText("");
-                ed.setText("");
-                try {
+                        System.out.println(" and now we'll set the text to be <"+string+">");
-                        ((StyledDocument) ed.getDocument()).insertString(0, string, ((StyledDocument) ed.getDocument()).getStyle("regular"));
-                        // ed.getDocument().insertString(0,