clarified image size;
authorwenzelm
Mon May 08 14:30:59 2017 +0200 (2017-05-08)
changeset 65773120ef768c84c
parent 65772 368399c5d87f
child 65774 1001fb86d7f7
clarified image size;
src/Pure/Admin/build_status.scala
src/Pure/Thy/html.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Mon May 08 14:30:37 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Mon May 08 14:30:59 2017 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  {
     1.5    private val default_target_dir = Path.explode("build_status")
     1.6    private val default_history_length = 30
     1.7 -  private val default_image_size = (640, 480)
     1.8 +  private val default_image_size = (800, 600)
     1.9  
    1.10  
    1.11    /* data profiles */
    1.12 @@ -253,7 +253,10 @@
    1.13                    HTML.bold(HTML.text("timing: ")) :: HTML.text(session.timing.message_resources),
    1.14                    HTML.bold(HTML.text("ML timing: ")) ::
    1.15                      HTML.text(session.ml_timing.message_resources))) ::
    1.16 -                session_plots.getOrElse(session.name, Nil).map(HTML.image(_)))))))
    1.17 +                session_plots.getOrElse(session.name, Nil).map(plot_name =>
    1.18 +                  HTML.image(plot_name) +
    1.19 +                    HTML.width(image_size._1 / 2) +
    1.20 +                    HTML.height(image_size._2 / 2)))))))
    1.21      }
    1.22  
    1.23      File.write(target_dir + Path.basic("index.html"),
     2.1 --- a/src/Pure/Thy/html.scala	Mon May 08 14:30:37 2017 +0200
     2.2 +++ b/src/Pure/Thy/html.scala	Mon May 08 14:30:59 2017 +0200
     2.3 @@ -83,7 +83,9 @@
     2.4  
     2.5    /* attributes */
     2.6  
     2.7 -  def id(s: String): Properties.Entry = ("id" -> s)
     2.8 +  def id(s: String): XML.Attribute = ("id" -> s)
     2.9 +  def width(w: Int): XML.Attribute = ("width" -> w.toString)
    2.10 +  def height(h: Int): XML.Attribute = ("height" -> h.toString)
    2.11  
    2.12  
    2.13    /* structured markup operators */