//# 6 errors, 320 messages
//#
/*
    //#VlcMediaSourcePlugin.java:1:1: class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#VlcMediaSourcePlugin.java:1:1: method: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init
 * Copyright (c) 2006-2009 Chris Smith, Shane Mc Cormack, Gregory Holmes
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 * SOFTWARE.
 */

package com.dmdirc.addons.mediasource_vlc;

import com.dmdirc.addons.nowplaying.MediaSource;
import com.dmdirc.addons.nowplaying.MediaSourceState;
import com.dmdirc.config.IdentityManager;
import com.dmdirc.config.prefs.PreferencesCategory;
import com.dmdirc.config.prefs.PreferencesManager;
import com.dmdirc.config.prefs.PreferencesSetting;
import com.dmdirc.config.prefs.PreferencesType;
import com.dmdirc.plugins.Plugin;
import com.dmdirc.util.Downloader;

import java.io.File;
import java.io.IOException;
import java.net.MalformedURLException;
import java.util.HashMap;
import java.util.List;
import java.util.Map;

/**
 * Retrieves information from VLC using its HTTP interface.
 * 
 * @author chris
 */
public class VlcMediaSourcePlugin extends Plugin implements MediaSource {
    //#VlcMediaSourcePlugin.java:47: method: void com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin()
    //#VlcMediaSourcePlugin.java:47: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.plugins.Plugin()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: void com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin()
    //#    unanalyzed callee: void com.dmdirc.plugins.Plugin()
    //#input(void com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin()): this
    //#output(void com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin()): new HashMap(VlcMediaSourcePlugin#1) num objects
    //#output(void com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin()): this.information
    //#new obj(void com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin()): new HashMap(VlcMediaSourcePlugin#1)
    //#post(void com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin()): this.information == &new HashMap(VlcMediaSourcePlugin#1)
    //#post(void com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin()): new HashMap(VlcMediaSourcePlugin#1) num objects == 1
    
    /** The information obtained from VLC. */
    private final Map<String, String> information
    //#VlcMediaSourcePlugin.java:50: end of method: void com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin()
            = new HashMap<String, String>();

    /** {@inheritDoc} */
    @Override
    public MediaSourceState getState() {
        if (fetchInformation()) {
    //#VlcMediaSourcePlugin.java:56: method: MediaSourceState com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getState()
    //#input(MediaSourceState getState()): ".old."._tainted
    //#input(MediaSourceState getState()): ".old.info.html"._tainted
    //#input(MediaSourceState getState()): "http:.."._tainted
    //#input(MediaSourceState getState()): "playlist_item_"._tainted
    //#input(MediaSourceState getState()): __Descendant_Table[com/dmdirc/addons/mediasource_vlc/VlcMediaSourcePlugin]
    //#input(MediaSourceState getState()): __Descendant_Table[others]
    //#input(MediaSourceState getState()): __Dispatch_Table.parseInformation(Ljava/util/List;Ljava/util/List;)V
    //#input(MediaSourceState getState()): com/dmdirc/addons/nowplaying/MediaSourceState.CLOSED
    //#input(MediaSourceState getState()): com/dmdirc/addons/nowplaying/MediaSourceState.NOTKNOWN
    //#input(MediaSourceState getState()): com/dmdirc/addons/nowplaying/MediaSourceState.PAUSED
    //#input(MediaSourceState getState()): com/dmdirc/addons/nowplaying/MediaSourceState.PLAYING
    //#input(MediaSourceState getState()): com/dmdirc/addons/nowplaying/MediaSourceState.STOPPED
    //#input(MediaSourceState getState()): this
    //#input(MediaSourceState getState()): this.__Tag
    //#input(MediaSourceState getState()): this.information
    //#output(MediaSourceState getState()): return_value
    //#pre[3] (MediaSourceState getState()): this.information != null
    //#pre[2] (MediaSourceState getState()): (soft) this.__Tag == com/dmdirc/addons/mediasource_vlc/VlcMediaSourcePlugin
    //#presumption(MediaSourceState getState()): java.util.Map:get(...)@57 != null
    //#post(MediaSourceState getState()): return_value in Addr_Set{&com.dmdirc.addons.nowplaying.MediaSourceState__static_init.new MediaSourceState(MediaSourceState__static_init#1),&com.dmdirc.addons.nowplaying.MediaSourceState__static_init.new MediaSourceState(MediaSourceState__static_init#5),&com.dmdirc.addons.nowplaying.MediaSourceState__static_init.new MediaSourceState(MediaSourceState__static_init#3),&com.dmdirc.addons.nowplaying.MediaSourceState__static_init.new MediaSourceState(MediaSourceState__static_init#4),&com.dmdirc.addons.nowplaying.MediaSourceState__static_init.new MediaSourceState(MediaSourceState__static_init#2)}
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:java.lang.String:length
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:java.lang.String:trim
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin:getDomain
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:java.lang.String:toLowerCase
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:java.util.Map:put
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:java.lang.Integer:toString
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:java.lang.String:equalsIgnoreCase
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:java.lang.String:endsWith
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:java.lang.String:isEmpty
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:java.util.Map:clear
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:com.dmdirc.config.IdentityManager:getGlobalConfig
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:com.dmdirc.config.ConfigManager:getOption
    //#unanalyzed(MediaSourceState getState()): Effects-of-calling:com.dmdirc.util.Downloader:getPage
    //#test_vector(MediaSourceState getState()): java.lang.String:equalsIgnoreCase(...)@58: {0}, {1}
    //#test_vector(MediaSourceState getState()): java.lang.String:equalsIgnoreCase(...)@60: {0}, {1}
    //#test_vector(MediaSourceState getState()): java.lang.String:equalsIgnoreCase(...)@62: {0}, {1}
            final String output = information.get("state");
            if (output.equalsIgnoreCase("stop")) {
                return MediaSourceState.STOPPED;
            } else if (output.equalsIgnoreCase("playing")) {
                return MediaSourceState.PLAYING;
            } else if (output.equalsIgnoreCase("paused")) {
                return MediaSourceState.PAUSED;
            } else {
                return MediaSourceState.NOTKNOWN;
            }
        } else {
            return MediaSourceState.CLOSED;
    //#VlcMediaSourcePlugin.java:68: end of method: MediaSourceState com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getState()
        }
    }

    /** {@inheritDoc} */
    @Override    
    public String getAppName() {
        return "VLC";
    //#VlcMediaSourcePlugin.java:75: method: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getAppName()
    //#output(String getAppName()): return_value
    //#post(String getAppName()): return_value == &"VLC"
    //#VlcMediaSourcePlugin.java:75: end of method: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getAppName()
    }

    /** {@inheritDoc} */
    @Override    
    public String getArtist() {
        return information.containsKey("artist") ? information.get("artist") :
    //#VlcMediaSourcePlugin.java:81: method: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getArtist()
    //#input(String getArtist()): "playlist_item_"._tainted
    //#input(String getArtist()): "unknown"._tainted
    //#input(String getArtist()): java.io.File.separator
    //#input(String getArtist()): java.io.File.separatorChar
    //#input(String getArtist()): this
    //#input(String getArtist()): this.information
    //#output(String getArtist()): return_value
    //#pre[2] (String getArtist()): this.information != null
    //#post(String getArtist()): init'ed(return_value)
    //#unanalyzed(String getArtist()): Effects-of-calling:java.util.Map:containsKey
    //#unanalyzed(String getArtist()): Effects-of-calling:java.util.Map:get
    //#unanalyzed(String getArtist()): Effects-of-calling:java.lang.Integer:parseInt
    //#unanalyzed(String getArtist()): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(String getArtist()): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(String getArtist()): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(String getArtist()): Effects-of-calling:java.lang.String:split
    //#unanalyzed(String getArtist()): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
    //#test_vector(String getArtist()): java.util.Map:containsKey(...)@81: {0}, {1}
    //#VlcMediaSourcePlugin.java:81: end of method: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getArtist()
                getFallbackArtist();
    }
     
    /**
     * Retrieves the fallback artist (parsed from the file name).
     * 
     * @return The fallback artist
     */
    private String getFallbackArtist() {
        String result = "unknown";
    //#VlcMediaSourcePlugin.java:91: method: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getFallbackArtist()
    //#input(String getFallbackArtist()): "playlist_item_"._tainted
    //#input(String getFallbackArtist()): "unknown"._tainted
    //#input(String getFallbackArtist()): java.io.File.separator
    //#input(String getFallbackArtist()): java.io.File.separatorChar
    //#input(String getFallbackArtist()): this
    //#input(String getFallbackArtist()): this.information
    //#output(String getFallbackArtist()): return_value
    //#pre[2] (String getFallbackArtist()): this.information != null
    //#presumption(String getFallbackArtist()): init'ed(java.io.File.separator)
    //#presumption(String getFallbackArtist()): init'ed(java.io.File.separatorChar)
    //#presumption(String getFallbackArtist()): java.util.Map:get(...)@96 != null
    //#post(String getFallbackArtist()): return_value == &"unknown"
    //#test_vector(String getFallbackArtist()): java.util.Map:containsKey(...)@93: {0}, {1}
        
        if (information.containsKey("playlist_current")) {
            try {
                final int item = Integer.parseInt(information.get("playlist_current"));
                String[] bits = information.get("playlist_item_" + item).split(
                        (File.separatorChar=='\\' ? "\\\\" : File.separator));
                result = bits[bits.length-1];
    //#VlcMediaSourcePlugin.java:98: ?use of default init
    //#    init'ed(bits.length)
    //#    severity: LOW
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: String getFallbackArtist()
    //#    basic block: bb_6
    //#    assertion: init'ed(bits.length)
    //#    VN: undefined
    //#    Expected: {-Inf..+Inf}
    //#    Bad: {Invalid}
    //#    Attribs:  Int  Bad only invalid
    //#VlcMediaSourcePlugin.java:98: ?!array index out of bounds
    //#    (bits.length - 1) >= 0
    //#    severity: HIGH
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: String getFallbackArtist()
    //#    basic block: bb_6
    //#    assertion: (bits.length - 1) >= 0
    //#    VN: undefined - 1
    //#    Expected: {0..+Inf}
    //#    Bad: {-1}
    //#    Attribs:  Int  Bad singleton  Bad overlaps +/-1000  Bad < Exp
    //#VlcMediaSourcePlugin.java:98: ?use of default init
    //#    init'ed(bits[(bits.length - 1)])
    //#    severity: SUPPRESSED
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: String getFallbackArtist()
    //#    basic block: bb_6
    //#    assertion: init'ed(bits[(bits.length - 1)])
    //#    VN: undefined
    //#    Expected: Univ-VN-Set
    //#    Bad: {Invalid}
    //#    Attribs:  Ptr  Bad only invalid
                bits = result.split("-");
    //#VlcMediaSourcePlugin.java:99: ?use of default init
    //#    init'ed(result)
    //#    severity: SUPPRESSED
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: String getFallbackArtist()
    //#    basic block: bb_6
    //#    assertion: init'ed(result)
    //#    VN: undefined
    //#    Expected: Univ-VN-Set
    //#    Bad: {Invalid}
    //#    Attribs:  Ptr  Bad only invalid
    //#VlcMediaSourcePlugin.java:99: ?null dereference
    //#    not_init'ed(result)
    //#    severity: MEDIUM
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: String getFallbackArtist()
    //#    basic block: bb_6
    //#    assertion: not_init'ed(result)
    //#    VN: undefined
    //#    Expected: Inverse{null} or Invalid
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
                if (bits.length > 1) {
    //#VlcMediaSourcePlugin.java:100: ?use of default init
    //#    init'ed(bits.length)
    //#    severity: LOW
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: String getFallbackArtist()
    //#    basic block: bb_6
    //#    assertion: init'ed(bits.length)
    //#    VN: undefined
    //#    Expected: {-Inf..+Inf}
    //#    Bad: {Invalid}
    //#    Attribs:  Int  Bad only invalid
    //#VlcMediaSourcePlugin.java:100: Warning: test always goes same way
    //#    Test predetermined because bits.length == 0
    //#    severity: LOW
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: String getFallbackArtist()
    //#    from bb: bb_6
    //#    live edge: bb_6-->bb_8
    //#    tested vn: undefined - 1
    //#    tested vn values: {-1}
                    result = bits[0];
    //#VlcMediaSourcePlugin.java:101: Warning: dead code
    //#    Dead code here because bits.length == 0
    //#    severity: LOW
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: String getFallbackArtist()
    //#    dead bb: bb_7
                } else {
                    // Whole filename is the title, so no artist is known.
                    result = "unknown";
                }
            } catch (NumberFormatException nfe) {
                // DO nothing
            }
        }
        
        return result;
    //#VlcMediaSourcePlugin.java:111: end of method: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getFallbackArtist()
    }

    /** {@inheritDoc} */
    @Override    
    public String getTitle() {
        return information.containsKey("title") ? information.get("title")
    //#VlcMediaSourcePlugin.java:117: method: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getTitle()
    //#input(String getTitle()): "playlist_item_"._tainted
    //#input(String getTitle()): "unknown"._tainted
    //#input(String getTitle()): java.io.File.separatorChar
    //#input(String getTitle()): this
    //#input(String getTitle()): this.information
    //#output(String getTitle()): java.lang.String:substring(...)._tainted
    //#output(String getTitle()): return_value
    //#new obj(String getTitle()): java.lang.String:substring(...)
    //#pre[2] (String getTitle()): this.information != null
    //#post(String getTitle()): java.lang.String:substring(...)._tainted == 0
    //#post(String getTitle()): init'ed(return_value)
    //#unanalyzed(String getTitle()): Effects-of-calling:java.util.Map:containsKey
    //#unanalyzed(String getTitle()): Effects-of-calling:java.util.Map:get
    //#unanalyzed(String getTitle()): Effects-of-calling:java.lang.Integer:parseInt
    //#unanalyzed(String getTitle()): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(String getTitle()): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(String getTitle()): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(String getTitle()): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
    //#unanalyzed(String getTitle()): Effects-of-calling:java.lang.String:lastIndexOf
    //#unanalyzed(String getTitle()): Effects-of-calling:java.lang.String:length
    //#unanalyzed(String getTitle()): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(String getTitle()): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(String getTitle()): Effects-of-calling:java.lang.String:trim
    //#test_vector(String getTitle()): java.util.Map:containsKey(...)@117: {0}, {1}
    //#VlcMediaSourcePlugin.java:117: end of method: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getTitle()
                : getFallbackTitle();
    }
    
    /**
     * Retrieves the fallback title (parsed from the file name).
     * 
     * @return The fallback title
     */
    private String getFallbackTitle() {
        String result = "unknown";
    //#VlcMediaSourcePlugin.java:127: method: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getFallbackTitle()
    //#input(String getFallbackTitle()): "playlist_item_"._tainted
    //#input(String getFallbackTitle()): "unknown"._tainted
    //#input(String getFallbackTitle()): java.io.File.separatorChar
    //#input(String getFallbackTitle()): this
    //#input(String getFallbackTitle()): this.information
    //#output(String getFallbackTitle()): java.lang.String:substring(...)._tainted
    //#output(String getFallbackTitle()): return_value
    //#new obj(String getFallbackTitle()): java.lang.String:substring(...)
    //#pre[2] (String getFallbackTitle()): this.information != null
    //#presumption(String getFallbackTitle()): init'ed(java.io.File.separatorChar)
    //#presumption(String getFallbackTitle()): java.lang.String:indexOf(...)@140 <= 4_294_967_294
    //#presumption(String getFallbackTitle()): java.util.Map:get(...)@133 != null
    //#post(String getFallbackTitle()): java.lang.String:substring(...)._tainted == 0
    //#post(String getFallbackTitle()): return_value != null
    //#test_vector(String getFallbackTitle()): java.lang.String:indexOf(...)@140: {-2_147_483_648..-1}, {0..4_294_967_294}
    //#test_vector(String getFallbackTitle()): java.util.Map:containsKey(...)@130: {0}, {1}
        
        // Title is unknown, lets guess using the filename
        if (information.containsKey("playlist_current")) {
            try {
                final int item = Integer.parseInt(information.get("playlist_current"));
                result = information.get("playlist_item_" + item);
                
                final int sepIndex = result.lastIndexOf(File.separatorChar);
                final int extIndex = result.lastIndexOf('.');
                result = result.substring(sepIndex,
                        extIndex > sepIndex ? extIndex : result.length());
                
                final int offset = result.indexOf('-');
                if (offset > -1) {
                    result = result.substring(offset + 1).trim();
                }
            } catch (NumberFormatException nfe) {
                // Do nothing
            }
        }
        
        return result;
    //#VlcMediaSourcePlugin.java:149: end of method: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getFallbackTitle()
    }

    /** {@inheritDoc} */
    @Override    
    public String getAlbum() {
        return information.containsKey("album/movie/show title")
    //#VlcMediaSourcePlugin.java:155: method: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getAlbum()
    //#input(String getAlbum()): this
    //#input(String getAlbum()): this.information
    //#output(String getAlbum()): return_value
    //#pre[2] (String getAlbum()): this.information != null
    //#post(String getAlbum()): init'ed(return_value)
    //#VlcMediaSourcePlugin.java:155: end of method: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getAlbum()
                ? information.get("album/movie/show title") : "unknown";
    }

    /** {@inheritDoc} */
    @Override    
    public String getLength() {
        // This is just seconds, could do with formatting.
        return information.containsKey("length") ? information.get("length")
    //#VlcMediaSourcePlugin.java:163: method: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getLength()
    //#input(String getLength()): this
    //#input(String getLength()): this.information
    //#output(String getLength()): return_value
    //#pre[2] (String getLength()): this.information != null
    //#post(String getLength()): init'ed(return_value)
    //#VlcMediaSourcePlugin.java:163: end of method: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getLength()
                : "unknown";
    }

    /** {@inheritDoc} */
    @Override    
    public String getTime() {
        // This is just seconds, could do with formatting.
        return information.containsKey("time") ? information.get("time")
    //#VlcMediaSourcePlugin.java:171: method: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getTime()
    //#input(String getTime()): this
    //#input(String getTime()): this.information
    //#output(String getTime()): return_value
    //#pre[2] (String getTime()): this.information != null
    //#post(String getTime()): init'ed(return_value)
    //#VlcMediaSourcePlugin.java:171: end of method: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getTime()
                : "unknown";
    }

    /** {@inheritDoc} */
    @Override    
    public String getFormat() {
        return information.containsKey("codec") ? information.get("codec")
    //#VlcMediaSourcePlugin.java:178: method: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getFormat()
    //#input(String getFormat()): this
    //#input(String getFormat()): this.information
    //#output(String getFormat()): return_value
    //#pre[2] (String getFormat()): this.information != null
    //#post(String getFormat()): init'ed(return_value)
    //#VlcMediaSourcePlugin.java:178: end of method: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getFormat()
                : "unknown";
    }

    /** {@inheritDoc} */
    @Override    
    public String getBitrate() {
        return information.containsKey("bitrate") ? information.get("bitrate")
    //#VlcMediaSourcePlugin.java:185: method: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getBitrate()
    //#input(String getBitrate()): this
    //#input(String getBitrate()): this.information
    //#output(String getBitrate()): return_value
    //#pre[2] (String getBitrate()): this.information != null
    //#post(String getBitrate()): init'ed(return_value)
    //#VlcMediaSourcePlugin.java:185: end of method: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.getBitrate()
                : "unknown";
    }

    /** {@inheritDoc} */
    @Override    
    public void onLoad() {
        // Do nothing
    }
    //#VlcMediaSourcePlugin.java:193: method: void com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.onLoad()
    //#VlcMediaSourcePlugin.java:193: end of method: void com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.onLoad()

    /** {@inheritDoc} */
    @Override    
    public void onUnload() {
        // Do nothing
    }
    //#VlcMediaSourcePlugin.java:199: method: void com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.onUnload()
    //#VlcMediaSourcePlugin.java:199: end of method: void com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.onUnload()

    /** {@inheritDoc} */
    @Override
    public void showConfig(final PreferencesManager manager) {
        final PreferencesCategory general = new PreferencesCategory("VLC Media Source",
    //#VlcMediaSourcePlugin.java:204: method: void com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.showConfig(PreferencesManager)
    //#VlcMediaSourcePlugin.java:204: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.config.prefs.PreferencesCategory(String, String, String)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: void showConfig(PreferencesManager)
    //#    unanalyzed callee: void com.dmdirc.config.prefs.PreferencesCategory(String, String, String)
    //#input(void showConfig(PreferencesManager)): com.dmdirc.config.prefs.PreferencesType.TEXT
    //#input(void showConfig(PreferencesManager)): manager
    //#input(void showConfig(PreferencesManager)): this
    //#pre[1] (void showConfig(PreferencesManager)): manager != null
    //#presumption(void showConfig(PreferencesManager)): com.dmdirc.config.prefs.PreferencesManager:getCategory(...)@213 != null
    //#presumption(void showConfig(PreferencesManager)): init'ed(com.dmdirc.config.prefs.PreferencesType.TEXT)
    //#unanalyzed(void showConfig(PreferencesManager)): Effects-of-calling:javax.swing.JPanel
    //#unanalyzed(void showConfig(PreferencesManager)): Effects-of-calling:net.miginfocom.swing.MigLayout
    //#unanalyzed(void showConfig(PreferencesManager)): Effects-of-calling:com.dmdirc.addons.mediasource_vlc.InstructionsPanel:setLayout
    //#unanalyzed(void showConfig(PreferencesManager)): Effects-of-calling:com.dmdirc.addons.ui_swing.components.text.TextLabel
    //#unanalyzed(void showConfig(PreferencesManager)): Effects-of-calling:com.dmdirc.addons.mediasource_vlc.InstructionsPanel:add
                "", "category-vlc");
        final PreferencesCategory instr = new PreferencesCategory("Instructions",
    //#VlcMediaSourcePlugin.java:206: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.config.prefs.PreferencesCategory(String, String, PreferencesInterface)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: void showConfig(PreferencesManager)
    //#    unanalyzed callee: void com.dmdirc.config.prefs.PreferencesCategory(String, String, PreferencesInterface)
                "", new InstructionsPanel());
        
        general.addSetting(new PreferencesSetting(PreferencesType.TEXT, 
    //#VlcMediaSourcePlugin.java:209: Warning: method not available - call not analyzed
    //#    call on String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin:getDomain()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: void showConfig(PreferencesManager)
    //#    unanalyzed callee: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin:getDomain()
    //#VlcMediaSourcePlugin.java:209: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.config.prefs.PreferencesSetting(PreferencesType, String, String, String, String)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: void showConfig(PreferencesManager)
    //#    unanalyzed callee: void com.dmdirc.config.prefs.PreferencesSetting(PreferencesType, String, String, String, String)
    //#VlcMediaSourcePlugin.java:209: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.config.prefs.PreferencesCategory:addSetting(PreferencesSetting)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: void showConfig(PreferencesManager)
    //#    unanalyzed callee: void com.dmdirc.config.prefs.PreferencesCategory:addSetting(PreferencesSetting)
                getDomain(), "host", "Hostname and port",
                "The host and port that VLC listens on for web connections"));
        
        manager.getCategory("Plugins").addSubCategory(general);
    //#VlcMediaSourcePlugin.java:213: Warning: method not available - call not analyzed
    //#    call on PreferencesCategory com.dmdirc.config.prefs.PreferencesManager:getCategory(String)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: void showConfig(PreferencesManager)
    //#    unanalyzed callee: PreferencesCategory com.dmdirc.config.prefs.PreferencesManager:getCategory(String)
    //#VlcMediaSourcePlugin.java:213: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.config.prefs.PreferencesCategory:addSubCategory(PreferencesCategory)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: void showConfig(PreferencesManager)
    //#    unanalyzed callee: void com.dmdirc.config.prefs.PreferencesCategory:addSubCategory(PreferencesCategory)
        general.addSubCategory(instr.setInline());
    //#VlcMediaSourcePlugin.java:214: Warning: method not available - call not analyzed
    //#    call on PreferencesCategory com.dmdirc.config.prefs.PreferencesCategory:setInline()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: void showConfig(PreferencesManager)
    //#    unanalyzed callee: PreferencesCategory com.dmdirc.config.prefs.PreferencesCategory:setInline()
    //#VlcMediaSourcePlugin.java:214: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.config.prefs.PreferencesCategory:addSubCategory(PreferencesCategory)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: void showConfig(PreferencesManager)
    //#    unanalyzed callee: void com.dmdirc.config.prefs.PreferencesCategory:addSubCategory(PreferencesCategory)
    }
    //#VlcMediaSourcePlugin.java:215: end of method: void com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.showConfig(PreferencesManager)
    
    /**
     * Attempts to fetch information from VLC's web interface.
     * 
     * @return True on success, false otherwise
     */
    private boolean fetchInformation() {
        information.clear();
    //#VlcMediaSourcePlugin.java:223: method: bool com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.fetchInformation()
    //#input(bool fetchInformation()): ".old."._tainted
    //#input(bool fetchInformation()): ".old.info.html"._tainted
    //#input(bool fetchInformation()): "http:.."._tainted
    //#input(bool fetchInformation()): "playlist_item_"._tainted
    //#input(bool fetchInformation()): __Descendant_Table[com/dmdirc/addons/mediasource_vlc/VlcMediaSourcePlugin]
    //#input(bool fetchInformation()): __Descendant_Table[others]
    //#input(bool fetchInformation()): __Dispatch_Table.parseInformation(Ljava/util/List;Ljava/util/List;)V
    //#input(bool fetchInformation()): this
    //#input(bool fetchInformation()): this.__Tag
    //#input(bool fetchInformation()): this.information
    //#output(bool fetchInformation()): return_value
    //#pre[3] (bool fetchInformation()): this.information != null
    //#pre[2] (bool fetchInformation()): (soft) this.__Tag == com/dmdirc/addons/mediasource_vlc/VlcMediaSourcePlugin
    //#presumption(bool fetchInformation()): com.dmdirc.config.IdentityManager:getGlobalConfig(...)@228 != null
    //#presumption(bool fetchInformation()): com.dmdirc.config.IdentityManager:getGlobalConfig(...)@231 != null
    //#presumption(bool fetchInformation()): com.dmdirc.util.Downloader:getPage(...)@228 != null
    //#presumption(bool fetchInformation()): com.dmdirc.util.Downloader:getPage(...)@231 != null
    //#post(bool fetchInformation()): init'ed(return_value)
    //#unanalyzed(bool fetchInformation()): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(bool fetchInformation()): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(bool fetchInformation()): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(bool fetchInformation()): Effects-of-calling:java.lang.String:length
    //#unanalyzed(bool fetchInformation()): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(bool fetchInformation()): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(bool fetchInformation()): Effects-of-calling:java.lang.String:trim
    //#unanalyzed(bool fetchInformation()): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(bool fetchInformation()): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(bool fetchInformation()): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(bool fetchInformation()): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(bool fetchInformation()): Effects-of-calling:java.lang.String:toLowerCase
    //#unanalyzed(bool fetchInformation()): Effects-of-calling:java.util.Map:put
    //#unanalyzed(bool fetchInformation()): Effects-of-calling:java.lang.Integer:toString
    //#unanalyzed(bool fetchInformation()): Effects-of-calling:java.lang.String:equalsIgnoreCase
    //#unanalyzed(bool fetchInformation()): Effects-of-calling:java.lang.String:endsWith
    //#unanalyzed(bool fetchInformation()): Effects-of-calling:java.lang.String:isEmpty
        List<String> res;
        List<String> res2;
        
        try {
            res = Downloader.getPage("http://" +
    //#VlcMediaSourcePlugin.java:228: Warning: method not available - call not analyzed
    //#    call on ConfigManager com.dmdirc.config.IdentityManager:getGlobalConfig()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: bool fetchInformation()
    //#    unanalyzed callee: ConfigManager com.dmdirc.config.IdentityManager:getGlobalConfig()
    //#VlcMediaSourcePlugin.java:228: Warning: method not available - call not analyzed
    //#    call on String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin:getDomain()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: bool fetchInformation()
    //#    unanalyzed callee: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin:getDomain()
    //#VlcMediaSourcePlugin.java:228: Warning: method not available - call not analyzed
    //#    call on String com.dmdirc.config.ConfigManager:getOption(String, String)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: bool fetchInformation()
    //#    unanalyzed callee: String com.dmdirc.config.ConfigManager:getOption(String, String)
    //#VlcMediaSourcePlugin.java:228: Warning: method not available - call not analyzed
    //#    call on List com.dmdirc.util.Downloader:getPage(String)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: bool fetchInformation()
    //#    unanalyzed callee: List com.dmdirc.util.Downloader:getPage(String)
                    IdentityManager.getGlobalConfig().getOption(getDomain(),
                    "host") + "/old/info.html");
            res2 = Downloader.getPage("http://" +
    //#VlcMediaSourcePlugin.java:231: Warning: method not available - call not analyzed
    //#    call on ConfigManager com.dmdirc.config.IdentityManager:getGlobalConfig()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: bool fetchInformation()
    //#    unanalyzed callee: ConfigManager com.dmdirc.config.IdentityManager:getGlobalConfig()
    //#VlcMediaSourcePlugin.java:231: Warning: method not available - call not analyzed
    //#    call on String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin:getDomain()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: bool fetchInformation()
    //#    unanalyzed callee: String com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin:getDomain()
    //#VlcMediaSourcePlugin.java:231: Warning: method not available - call not analyzed
    //#    call on String com.dmdirc.config.ConfigManager:getOption(String, String)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: bool fetchInformation()
    //#    unanalyzed callee: String com.dmdirc.config.ConfigManager:getOption(String, String)
    //#VlcMediaSourcePlugin.java:231: Warning: method not available - call not analyzed
    //#    call on List com.dmdirc.util.Downloader:getPage(String)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
    //#    method: bool fetchInformation()
    //#    unanalyzed callee: List com.dmdirc.util.Downloader:getPage(String)
                    IdentityManager.getGlobalConfig().getOption(getDomain(),
                    "host") + "/old/");
        } catch (MalformedURLException ex) {
            return false;
        } catch (IOException ex) {
            return false;
        }
        
        parseInformation(res, res2);
        
        return true;
    //#VlcMediaSourcePlugin.java:242: end of method: bool com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.fetchInformation()
    }
    
    /**
     * Parses the information from the two pages obtained from VLC's web
     * interface.
     * 
     * @param res The first page of VLC info (/old/info.html)
     * @param res2 The second page of VLC info (/old/)
     */
    protected void parseInformation(final List<String> res,
            final List<String> res2) {
        for (String line : res) {
    //#VlcMediaSourcePlugin.java:254: method: void com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.parseInformation(List, List)
    //#input(void parseInformation(List, List)): "playlist_item_"._tainted
    //#input(void parseInformation(List, List)): res
    //#input(void parseInformation(List, List)): res2
    //#input(void parseInformation(List, List)): this
    //#input(void parseInformation(List, List)): this.information
    //#pre[1] (void parseInformation(List, List)): res != null
    //#pre[2] (void parseInformation(List, List)): res2 != null
    //#pre[4] (void parseInformation(List, List)): (soft) this.information != null
    //#presumption(void parseInformation(List, List)): java.lang.String:indexOf(...)@258 <= 4_294_967_294
    //#presumption(void parseInformation(List, List)): java.lang.String:indexOf(...)@302 <= 4_294_967_294
    //#presumption(void parseInformation(List, List)): java.util.Iterator:next(...)@254 != null
    //#presumption(void parseInformation(List, List)): java.util.Iterator:next(...)@270 != null
    //#test_vector(void parseInformation(List, List)): java.lang.String:endsWith(...)@285: {0}, {1}
    //#test_vector(void parseInformation(List, List)): java.lang.String:equalsIgnoreCase(...)@277: {0}, {1}
    //#test_vector(void parseInformation(List, List)): java.lang.String:equalsIgnoreCase(...)@279: {0}, {1}
    //#test_vector(void parseInformation(List, List)): java.lang.String:equalsIgnoreCase(...)@297: {0}, {1}
    //#test_vector(void parseInformation(List, List)): java.lang.String:isEmpty(...)@288: {1}, {0}
    //#test_vector(void parseInformation(List, List)): java.lang.String:startsWith(...)@257: {0}, {1}
    //#test_vector(void parseInformation(List, List)): java.lang.String:startsWith(...)@274: {0}, {1}
    //#test_vector(void parseInformation(List, List)): java.lang.String:startsWith(...)@281: {0}, {1}
    //#test_vector(void parseInformation(List, List)): java.lang.String:startsWith(...)@299: {0}, {1}
    //#test_vector(void parseInformation(List, List)): java.lang.String:startsWith(...)@301: {0}, {1}
    //#test_vector(void parseInformation(List, List)): java.util.Iterator:hasNext(...)@254: {0}, {1}
    //#test_vector(void parseInformation(List, List)): java.util.Iterator:hasNext(...)@270: {0}, {1}
            final String tline = line.trim();
            
            if (tline.startsWith("<li>")) {
                final int colon = tline.indexOf(':');
                final String key = tline.substring(5, colon).trim().toLowerCase();
                final String value = tline.substring(colon + 1, tline.length() - 5).trim();
                
                information.put(key, value);
            }
        }
        
        boolean isPlaylist = false;
        boolean isCurrent = false;
        boolean isItem = false;
        int playlistItem = 0;
        for (String line : res2) {
            final String tline = line.trim();
            
            if (isPlaylist) {
                if (tline.startsWith("</ul>")) {
                    isPlaylist = false;
                    information.put("playlist_items", Integer.toString(playlistItem));
                } else if (tline.equalsIgnoreCase("<strong>")) {
                    isCurrent = true;
                } else if (tline.equalsIgnoreCase("</strong>")) {
                    isCurrent = false;
                } else if (tline.startsWith("<a href=\"?control=play&amp")) {
                    isItem = true;
                } else if (isItem) {
                    String itemname = tline;
                    if (itemname.endsWith("</a>")) {
                        itemname = itemname.substring(0, itemname.length()-4);
                    }
                    if (!itemname.isEmpty()) {
                        if (isCurrent) {
                            information.put("playlist_current", Integer.toString(playlistItem));
                        }
                        information.put("playlist_item_"+Integer.toString(playlistItem++),
                                itemname);
                    }
                    isItem = false;
                }
            } else if (tline.equalsIgnoreCase("<!-- Playlist -->")) {
                isPlaylist = true;
            } else if (tline.startsWith("State:")) {
                information.put("state", tline.substring(6, tline.indexOf('<')).trim());
            } else if (tline.startsWith("got_")) {
                final int equals = tline.indexOf('=');
                
                information.put(tline.substring(4, equals).trim(),
                        tline.substring(equals + 1, tline.length() - 1).trim());
            }
        }
    }
    //#VlcMediaSourcePlugin.java:308: end of method: void com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.parseInformation(List, List)

}
    //#output(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Descendant_Table[com/dmdirc/addons/mediasource_vlc/VlcMediaSourcePlugin]
    //#output(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.fetchInformation()Z
    //#output(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getAlbum()Ljava/lang/String;
    //#output(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getAppName()Ljava/lang/String;
    //#output(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getArtist()Ljava/lang/String;
    //#output(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getBitrate()Ljava/lang/String;
    //#output(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getFallbackArtist()Ljava/lang/String;
    //#output(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getFallbackTitle()Ljava/lang/String;
    //#output(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getFormat()Ljava/lang/String;
    //#output(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getLength()Ljava/lang/String;
    //#output(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getState()Lcom/dmdirc/addons/nowplaying/MediaSourceState;
    //#output(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getTime()Ljava/lang/String;
    //#output(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getTitle()Ljava/lang/String;
    //#output(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.onLoad()V
    //#output(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.onUnload()V
    //#output(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.parseInformation(Ljava/util/List;Ljava/util/List;)V
    //#output(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.showConfig(Lcom/dmdirc/config/prefs/PreferencesManager;)V
    //#output(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): com/dmdirc/addons/nowplaying/MediaSource.__Descendant_Table[com/dmdirc/addons/mediasource_vlc/VlcMediaSourcePlugin]
    //#post(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Descendant_Table[com/dmdirc/addons/mediasource_vlc/VlcMediaSourcePlugin] == &__Dispatch_Table
    //#post(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): com/dmdirc/addons/nowplaying/MediaSource.__Descendant_Table[com/dmdirc/addons/mediasource_vlc/VlcMediaSourcePlugin] == &__Dispatch_Table
    //#post(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.fetchInformation()Z == &fetchInformation
    //#post(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getAlbum()Ljava/lang/String; == &getAlbum
    //#post(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getAppName()Ljava/lang/String; == &getAppName
    //#post(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getArtist()Ljava/lang/String; == &getArtist
    //#post(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getBitrate()Ljava/lang/String; == &getBitrate
    //#post(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getFallbackArtist()Ljava/lang/String; == &getFallbackArtist
    //#post(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getFallbackTitle()Ljava/lang/String; == &getFallbackTitle
    //#post(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getFormat()Ljava/lang/String; == &getFormat
    //#post(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getLength()Ljava/lang/String; == &getLength
    //#post(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getState()Lcom/dmdirc/addons/nowplaying/MediaSourceState; == &getState
    //#post(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getTime()Ljava/lang/String; == &getTime
    //#post(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.getTitle()Ljava/lang/String; == &getTitle
    //#post(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.onLoad()V == &onLoad
    //#post(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.onUnload()V == &onUnload
    //#post(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.parseInformation(Ljava/util/List;Ljava/util/List;)V == &parseInformation
    //#post(com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init): __Dispatch_Table.showConfig(Lcom/dmdirc/config/prefs/PreferencesManager;)V == &showConfig
    //#VlcMediaSourcePlugin.java:: end of method: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin.com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin__static_init
    //#VlcMediaSourcePlugin.java:: end of class: com.dmdirc.addons.mediasource_vlc.VlcMediaSourcePlugin
