New html_print_logo() API function

This makes it easier for people to add the logo in an include file,
since it is not shown anymore when $g_top_include_page is set.

The html_top_banner() function was modified to use the new API.

Fixes #21087

core/html_api.php

@@ -489,37 +489,44 @@ function html_body_begin() {
 }
 
 /**
- * (9) Print a user-defined banner at the top of the page if there is one.
+ * Prints the logo with an URL link.
+ * @param string $p_logo Path to the logo image. If not specified, will get it
+ *                       from $g_logo_image
  * @return void
  */
-function html_top_banner() {
-	$t_page = config_get( 'top_include_page' );
-	$t_logo_image = config_get( 'logo_image' );
-	$t_logo_url = config_get( 'logo_url' );
-
-	if( is_blank( $t_logo_image ) ) {
-		$t_show_logo = false;
-	} else {
-		$t_show_logo = true;
-		if( is_blank( $t_logo_url ) ) {
-			$t_show_url = false;
-		} else {
-			$t_show_url = true;
-		}
+function html_print_logo($p_logo = null) {
+	if( !$p_logo ) {
+		$p_logo = config_get( 'logo_image' );
 	}
 
-	if( !is_blank( $t_page ) && file_exists( $t_page ) && !is_dir( $t_page ) ) {
-		include( $t_page );
-	} else if( $t_show_logo ) {
-		echo '<div id="banner">';
+	if( !is_blank( $p_logo ) ) {
+		$t_logo_url = config_get( 'logo_url' );
+		$t_show_url = !is_blank( $t_logo_url );
+
 		if( $t_show_url ) {
-			echo '<a id="logo-link" href="', config_get( 'logo_url' ), '">';
+			echo '<a id="logo-link" href="' . $t_logo_url . '">';
 		}
 		$t_alternate_text = string_html_specialchars( config_get( 'window_title' ) );
-		echo '<img id="logo-image" alt="', $t_alternate_text, '" src="' . helper_mantis_url( $t_logo_image ) . '" />';
+		echo '<img id="logo-image" alt="'. $t_alternate_text . '" src="' . helper_mantis_url( $p_logo ) . '" />';
 		if( $t_show_url ) {
 			echo '</a>';
 		}
+	}
+}
+
+/**
+ * (9) Print a user-defined banner at the top of the page if there is one.
+ * @return void
+ */
+function html_top_banner() {
+	$t_page = config_get( 'top_include_page' );
+	$t_logo_image = config_get( 'logo_image' );
+
+	if( !is_blank( $t_page ) && file_exists( $t_page ) && !is_dir( $t_page ) ) {
+		include( $t_page );
+	} else if( !is_blank( $t_logo_image ) ) {
+		echo '<div id="banner">';
+		html_print_logo( $t_logo_image );
 		echo '</div>';
 	}