* Use gtksourceview2 instead of gtksourceview default tip
authorthib
Fri Oct 31 22:09:43 2008 +0000 (2008-10-31)
changeset 14842dfd8f1537
parent 13 3c2545658866
* Use gtksourceview2 instead of gtksourceview
* Little changes in the toolbar's default display
page.py
source_page.py
toolbar.py
     1.1 --- a/page.py	Fri Oct 31 20:21:36 2008 +0000
     1.2 +++ b/page.py	Fri Oct 31 22:09:43 2008 +0000
     1.3 @@ -72,6 +72,8 @@
     1.4      def open(self, url):
     1.5          if url.startswith('javascript:'):
     1.6              self._browser.execute_script(url[11:])
     1.7 +        elif url == '':
     1.8 +            pass
     1.9          else:
    1.10              if not '://' in url:
    1.11                  url = 'http://'+url
    1.12 @@ -142,7 +144,8 @@
    1.13          if frame.get_parent() is None:
    1.14              self.uri = frame.get_uri()
    1.15              self.title = frame.get_title()
    1.16 -            self.emit('title-changed', self.title)
    1.17 +            if self.title is not None:
    1.18 +                self.emit('title-changed', self.title)
    1.19  
    1.20  
    1.21      def handle_scroll_adjustments(self, page, hadjustment, vadjustment):
     2.1 --- a/source_page.py	Fri Oct 31 20:21:36 2008 +0000
     2.2 +++ b/source_page.py	Fri Oct 31 22:09:43 2008 +0000
     2.3 @@ -1,15 +1,43 @@
     2.4  import gobject
     2.5  import gtk
     2.6 -import gtksourceview
     2.7 +import gtksourceview2
     2.8  from urllib import FancyURLopener
     2.9  
    2.10 -class SourceView(gtksourceview.SourceView):
    2.11 +class LanguageManager(object):
    2.12 +    cache = None
    2.13 +    def __new__(cls):
    2.14 +        if cls.cache:
    2.15 +            return cls.cache
    2.16 +        self = object.__new__(cls)
    2.17 +
    2.18 +        lang_manager = gtksourceview2.language_manager_get_default()
    2.19 +        mime_types = dict()
    2.20 +        ids = lang_manager.get_language_ids()
    2.21 +        for id_ in ids:
    2.22 +            lang = lang_manager.get_language(id_)
    2.23 +            for type_ in lang.get_mime_types():
    2.24 +                mime_types[type_] = lang
    2.25 +        self._mime_types = mime_types
    2.26 +
    2.27 +        cls.cache = self
    2.28 +        return self
    2.29 +
    2.30 +
    2.31 +    def get_language_from_mime_type(self, mime_type):
    2.32 +        if mime_type in self._mime_types:
    2.33 +            return self._mime_types[mime_type]
    2.34 +        elif 'xml' in mime_type:
    2.35 +            return self._mime_types['text/xml']
    2.36 +        else:
    2.37 +            return None
    2.38 +
    2.39 +class SourceView(gtksourceview2.View):
    2.40      def __init__(self):
    2.41 -        self.source_buffer = gtksourceview.SourceBuffer()
    2.42 +        self.source_buffer = gtksourceview2.Buffer()
    2.43  
    2.44 -        self.source_buffer.set_highlight(True)
    2.45 +        self.source_buffer.set_highlight_syntax(True)
    2.46  
    2.47 -        gtksourceview.SourceView.__init__(self, self.source_buffer)
    2.48 +        gtksourceview2.View.__init__(self, self.source_buffer)
    2.49          self.set_show_line_numbers(True)
    2.50          self.set_editable(False)
    2.51  
    2.52 @@ -25,10 +53,8 @@
    2.53          else:
    2.54              mime_type = content_type
    2.55  
    2.56 -        language_manager = gtksourceview.SourceLanguagesManager()
    2.57 +        language_manager = LanguageManager()
    2.58          language = language_manager.get_language_from_mime_type(mime_type)
    2.59 -        if language is None and 'xml' in mime_type:
    2.60 -            language = language_manager.get_language_from_mime_type('text/xml')
    2.61  
    2.62          self.source_buffer.set_language(language)
    2.63  
     3.1 --- a/toolbar.py	Fri Oct 31 20:21:36 2008 +0000
     3.2 +++ b/toolbar.py	Fri Oct 31 22:09:43 2008 +0000
     3.3 @@ -30,17 +30,18 @@
     3.4  
     3.5          # FIXME: Back button
     3.6          button = BackForwardButton(0)
     3.7 +        button.set_sensitive(False)
     3.8          self._back_button = button
     3.9          self.insert(button, -1)
    3.10  
    3.11          # FIXME: Forward button
    3.12          button = BackForwardButton(1)
    3.13 +        button.set_sensitive(False)
    3.14          self._forward_button = button
    3.15          self.insert(button, -1)
    3.16  
    3.17          # FIXME: Stop/Refresh button
    3.18          self._stop_button = StopRefreshButton()
    3.19 -        #button.set_sensitive(False)
    3.20          self.insert(self._stop_button, -1)
    3.21  
    3.22          # FIXME: Home button
    3.23 @@ -109,7 +110,7 @@
    3.24      }
    3.25      def __init__(self):
    3.26          gtk.ToolButton.__init__(self, gtk.STOCK_STOP)
    3.27 -        self.mode = gtk.STOCK_STOP
    3.28 +        self.set_refresh()
    3.29          self.connect('clicked', self.on_click)
    3.30  
    3.31      def on_click(self, widget, data=None):