//# 0 errors, 67 messages
//#
/*
    //#ThemeIdentity.java:1:1: class: com.dmdirc.ui.themes.ThemeIdentity
    //#ThemeIdentity.java:1:1: method: com.dmdirc.ui.themes.ThemeIdentity.com.dmdirc.ui.themes.ThemeIdentity__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.ui.themes;

import com.dmdirc.config.Identity;
import com.dmdirc.config.InvalidIdentityFileException;

import java.io.IOException;
import java.io.InputStream;

/**
 * An identity that only claims to know about settings under the UI domain,
 * for use with themes.
 *
 * @author Chris
 */
public class ThemeIdentity extends Identity {
    
    /**
     * A version number for this class. It should be changed whenever the class
     * structure is changed (or anything else that would prevent serialized
     * objects being unserialized with the new class).
     */
    private static final long serialVersionUID = 1;
    
    /** The theme that owns this identity. */
    private final Theme theme;
    
    /**
     * Creates a new instance of ThemeIdentity.
     *
     * @param stream The input stream to read the identity from.
     * @param theme The theme that owns this identity
     * @throws InvalidIdentityFileException Missing required properties
     * @throws IOException Input/output exception
     */
    public ThemeIdentity(final InputStream stream, final Theme theme) throws IOException,
            InvalidIdentityFileException {
        super(stream, true);
    //#ThemeIdentity.java:59: method: void com.dmdirc.ui.themes.ThemeIdentity.com.dmdirc.ui.themes.ThemeIdentity(InputStream, Theme)
    //#ThemeIdentity.java:59: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.config.Identity(InputStream, bool)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.themes.ThemeIdentity
    //#    method: void com.dmdirc.ui.themes.ThemeIdentity(InputStream, Theme)
    //#    unanalyzed callee: void com.dmdirc.config.Identity(InputStream, bool)
    //#input(void com.dmdirc.ui.themes.ThemeIdentity(InputStream, Theme)): stream
    //#input(void com.dmdirc.ui.themes.ThemeIdentity(InputStream, Theme)): theme
    //#input(void com.dmdirc.ui.themes.ThemeIdentity(InputStream, Theme)): this
    //#output(void com.dmdirc.ui.themes.ThemeIdentity(InputStream, Theme)): this.myTarget
    //#output(void com.dmdirc.ui.themes.ThemeIdentity(InputStream, Theme)): this.theme
    //#presumption(void com.dmdirc.ui.themes.ThemeIdentity(InputStream, Theme)): this.myTarget@59 != null
    //#post(void com.dmdirc.ui.themes.ThemeIdentity(InputStream, Theme)): this.myTarget != null
    //#post(void com.dmdirc.ui.themes.ThemeIdentity(InputStream, Theme)): this.theme == theme
    //#post(void com.dmdirc.ui.themes.ThemeIdentity(InputStream, Theme)): init'ed(this.theme)
        
        myTarget.setTheme();
    //#ThemeIdentity.java:61: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.config.ConfigTarget:setTheme()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.themes.ThemeIdentity
    //#    method: void com.dmdirc.ui.themes.ThemeIdentity(InputStream, Theme)
    //#    unanalyzed callee: void com.dmdirc.config.ConfigTarget:setTheme()
        this.theme = theme;
    }
    //#ThemeIdentity.java:63: end of method: void com.dmdirc.ui.themes.ThemeIdentity.com.dmdirc.ui.themes.ThemeIdentity(InputStream, Theme)
    
    /** {@inheritDoc} */
    @Override @Deprecated
    public boolean hasOption(final String domain, final String option) {
        if (domain.equalsIgnoreCase("ui") || domain.equalsIgnoreCase("identity")
    //#ThemeIdentity.java:68: method: bool com.dmdirc.ui.themes.ThemeIdentity.hasOption(String, String)
    //#input(bool hasOption(String, String)): domain
    //#input(bool hasOption(String, String)): option
    //#input(bool hasOption(String, String)): this
    //#output(bool hasOption(String, String)): return_value
    //#pre[1] (bool hasOption(String, String)): domain != null
    //#post(bool hasOption(String, String)): init'ed(return_value)
    //#test_vector(bool hasOption(String, String)): java.lang.String:equalsIgnoreCase(...)@68: {1}, {0}
    //#test_vector(bool hasOption(String, String)): java.lang.String:equalsIgnoreCase(...)@68: {0}, {1}
                || domain.equalsIgnoreCase("icon")  || domain.equalsIgnoreCase("theme")
                || domain.equalsIgnoreCase("formatter") || domain.equalsIgnoreCase("colour")) {
            return super.hasOption(domain, option);
    //#ThemeIdentity.java:71: Warning: method not available - call not analyzed
    //#    call on bool com.dmdirc.config.Identity:hasOption(String, String)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.themes.ThemeIdentity
    //#    method: bool hasOption(String, String)
    //#    unanalyzed callee: bool com.dmdirc.config.Identity:hasOption(String, String)
        } else {
            return false;
    //#ThemeIdentity.java:73: end of method: bool com.dmdirc.ui.themes.ThemeIdentity.hasOption(String, String)
        }
    }

    /** {@inheritDoc} */
    @Override
    public String getOption(final String domain, final String option) {
        final String result = super.getOption(domain, option);
    //#ThemeIdentity.java:80: method: String com.dmdirc.ui.themes.ThemeIdentity.getOption(String, String)
    //#ThemeIdentity.java:80: Warning: method not available - call not analyzed
    //#    call on String com.dmdirc.config.Identity:getOption(String, String)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.themes.ThemeIdentity
    //#    method: String getOption(String, String)
    //#    unanalyzed callee: String com.dmdirc.config.Identity:getOption(String, String)
    //#input(String getOption(String, String)): com/dmdirc/ui/themes/Theme.__Descendant_Table[com/dmdirc/ui/themes/Theme]
    //#input(String getOption(String, String)): com/dmdirc/ui/themes/Theme.__Descendant_Table[others]
    //#input(String getOption(String, String)): com/dmdirc/ui/themes/Theme.__Dispatch_Table.getFileName(Z)Ljava/lang/String;
    //#input(String getOption(String, String)): domain
    //#input(String getOption(String, String)): option
    //#input(String getOption(String, String)): this
    //#input(String getOption(String, String)): this.theme
    //#input(String getOption(String, String)): this.theme.__Tag
    //#input(String getOption(String, String)): this.theme.file
    //#output(String getOption(String, String)): return_value
    //#pre[4] (String getOption(String, String)): (soft) this.theme != null
    //#pre[5] (String getOption(String, String)): (soft) this.theme.__Tag == com/dmdirc/ui/themes/Theme
    //#pre[6] (String getOption(String, String)): (soft) this.theme.file != null
    //#post(String getOption(String, String)): init'ed(return_value)
    //#unanalyzed(String getOption(String, String)): Effects-of-calling:java.io.File:getName
    //#unanalyzed(String getOption(String, String)): Effects-of-calling:java.lang.String:length
    //#unanalyzed(String getOption(String, String)): Effects-of-calling:java.lang.String:substring
    //#test_vector(String getOption(String, String)): com.dmdirc.config.Identity:getOption(...)@80: Inverse{null}, Addr_Set{null}
        
        if (result == null) {
            return result;
        } else {
            return result.replaceAll("\\$theme", theme.getFileName(false));
    //#ThemeIdentity.java:85: end of method: String com.dmdirc.ui.themes.ThemeIdentity.getOption(String, String)
        }
    }

    /** {@inheritDoc} */
    @Override
    public String getName() {
        return "Theme UI config: " + super.getName();
    //#ThemeIdentity.java:92: method: String com.dmdirc.ui.themes.ThemeIdentity.getName()
    //#ThemeIdentity.java:92: Warning: method not available - call not analyzed
    //#    call on String com.dmdirc.config.Identity:getName()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.themes.ThemeIdentity
    //#    method: String getName()
    //#    unanalyzed callee: String com.dmdirc.config.Identity:getName()
    //#input(String getName()): "Theme UI config: "._tainted
    //#input(String getName()): this
    //#output(String getName()): java.lang.StringBuilder:toString(...)._tainted
    //#output(String getName()): return_value
    //#new obj(String getName()): java.lang.StringBuilder:toString(...)
    //#post(String getName()): java.lang.StringBuilder:toString(...)._tainted == 0
    //#post(String getName()): return_value == &java.lang.StringBuilder:toString(...)
    //#ThemeIdentity.java:92: end of method: String com.dmdirc.ui.themes.ThemeIdentity.getName()
    }
    
}
    //#output(com.dmdirc.ui.themes.ThemeIdentity__static_init): __Descendant_Table[com/dmdirc/ui/themes/ThemeIdentity]
    //#output(com.dmdirc.ui.themes.ThemeIdentity__static_init): __Dispatch_Table.getName()Ljava/lang/String;
    //#output(com.dmdirc.ui.themes.ThemeIdentity__static_init): __Dispatch_Table.getOption(Ljava/lang/String;Ljava/lang/String;)Ljava/lang/String;
    //#output(com.dmdirc.ui.themes.ThemeIdentity__static_init): __Dispatch_Table.hasOption(Ljava/lang/String;Ljava/lang/String;)Z
    //#post(com.dmdirc.ui.themes.ThemeIdentity__static_init): __Descendant_Table[com/dmdirc/ui/themes/ThemeIdentity] == &__Dispatch_Table
    //#post(com.dmdirc.ui.themes.ThemeIdentity__static_init): __Dispatch_Table.getName()Ljava/lang/String; == &getName
    //#post(com.dmdirc.ui.themes.ThemeIdentity__static_init): __Dispatch_Table.getOption(Ljava/lang/String;Ljava/lang/String;)Ljava/lang/String; == &getOption
    //#post(com.dmdirc.ui.themes.ThemeIdentity__static_init): __Dispatch_Table.hasOption(Ljava/lang/String;Ljava/lang/String;)Z == &hasOption
    //#ThemeIdentity.java:: end of method: com.dmdirc.ui.themes.ThemeIdentity.com.dmdirc.ui.themes.ThemeIdentity__static_init
    //#ThemeIdentity.java:: end of class: com.dmdirc.ui.themes.ThemeIdentity
