# HG changeset patch # User wenzelm # Date 1274476900 -7200 # Node ID d03b5745742119974b665fdb8d7410eda07bd6ac # Parent 8f9f3d61ca8c20b02302a70be62c9fdb461949b2# Parent d014976dd69019e94244cd6d34819ec6cf224b1e merged diff -r 8f9f3d61ca8c -r d03b57457421 lib/html/isabelle.css --- a/lib/html/isabelle.css Fri May 21 17:16:16 2010 +0200 +++ b/lib/html/isabelle.css Fri May 21 23:21:40 2010 +0200 @@ -1,4 +1,4 @@ -/* css style file for Isabelle XHTML/XML output */ +/* style file for Isabelle XHTML/XML output */ body { background-color: #FFFFFF; } diff -r 8f9f3d61ca8c -r d03b57457421 src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Fri May 21 17:16:16 2010 +0200 +++ b/src/Pure/Concurrent/future.ML Fri May 21 23:21:40 2010 +0200 @@ -170,12 +170,14 @@ fun future_job group (e: unit -> 'a) = let val result = Single_Assignment.var "future" : 'a result; + val pos = Position.thread_data (); fun job ok = let val res = if ok then Exn.capture (fn () => - Multithreading.with_attributes Multithreading.private_interrupts (fn _ => e ())) () + Multithreading.with_attributes Multithreading.private_interrupts + (fn _ => Position.setmp_thread_data pos e ())) () else Exn.Exn Exn.Interrupt; in assign_result group result res end; in (result, job) end; diff -r 8f9f3d61ca8c -r d03b57457421 src/Pure/General/position.ML --- a/src/Pure/General/position.ML Fri May 21 17:16:16 2010 +0200 +++ b/src/Pure/General/position.ML Fri May 21 23:21:40 2010 +0200 @@ -173,9 +173,7 @@ fun thread_data () = the_default none (Thread.getLocal tag); -fun setmp_thread_data pos f x = - if ! Output.debugging then f x - else Library.setmp_thread_data tag (thread_data ()) pos f x; +fun setmp_thread_data pos = Library.setmp_thread_data tag (thread_data ()) pos; end; diff -r 8f9f3d61ca8c -r d03b57457421 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Fri May 21 17:16:16 2010 +0200 +++ b/src/Pure/IsaMakefile Fri May 21 23:21:40 2010 +0200 @@ -12,8 +12,6 @@ ## global settings -SHELL = /bin/bash - SRC = $(ISABELLE_HOME)/src OUT = $(ISABELLE_OUTPUT) LOG = $(OUT)/log diff -r 8f9f3d61ca8c -r d03b57457421 src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Fri May 21 17:16:16 2010 +0200 +++ b/src/Pure/Isar/calculation.ML Fri May 21 23:21:40 2010 +0200 @@ -14,7 +14,8 @@ val sym_del: attribute val symmetric: attribute val also: thm list option -> bool -> Proof.state -> Proof.state Seq.seq - val also_cmd: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq + val also_cmd: (Facts.ref * Attrib.src list) list option -> + bool -> Proof.state -> Proof.state Seq.seq val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.seq val finally_cmd: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq @@ -27,7 +28,7 @@ (** calculation data **) -structure CalculationData = Generic_Data +structure Data = Generic_Data ( type T = (thm Item_Net.T * thm list) * (thm list * int) option; val empty = ((Thm.elim_rules, []), NONE); @@ -37,7 +38,7 @@ ); fun print_rules ctxt = - let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in + let val ((trans, sym), _) = Data.get (Context.Proof ctxt) in [Pretty.big_list "transitivity rules:" (map (Display.pretty_thm ctxt) (Item_Net.content trans)), Pretty.big_list "symmetry rules:" (map (Display.pretty_thm ctxt) sym)] @@ -48,7 +49,7 @@ (* access calculation *) fun get_calculation state = - (case #2 (CalculationData.get (Context.Proof (Proof.context_of state))) of + (case #2 (Data.get (Context.Proof (Proof.context_of state))) of NONE => NONE | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE); @@ -56,7 +57,7 @@ fun put_calculation calc = `Proof.level #-> (fn lev => Proof.map_context (Context.proof_map - (CalculationData.map (apsnd (K (Option.map (rpair lev) calc)))))) + (Data.map (apsnd (K (Option.map (rpair lev) calc)))))) #> Proof.put_thms false (calculationN, calc); @@ -65,22 +66,22 @@ (* add/del rules *) -val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.update); -val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.remove); +val trans_add = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.update); +val trans_del = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.remove); val sym_add = - Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm) + Thm.declaration_attribute (Data.map o apfst o apsnd o Thm.add_thm) #> Context_Rules.elim_query NONE; val sym_del = - Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.del_thm) + Thm.declaration_attribute (Data.map o apfst o apsnd o Thm.del_thm) #> Context_Rules.rule_del; (* symmetric *) val symmetric = Thm.rule_attribute (fn x => fn th => - (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of + (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (Data.get x)))) of ([th'], _) => Drule.zero_var_indexes th' | ([], _) => raise THM ("symmetric: no unifiers", 1, [th]) | _ => raise THM ("symmetric: multiple unifiers", 1, [th]))); @@ -103,28 +104,31 @@ (** proof commands **) -fun err_if b msg = if b then error msg else (); - fun assert_sane final = if final then Proof.assert_forward else Proof.assert_forward_or_chain; -fun maintain_calculation false calc = put_calculation (SOME calc) - | maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc; - -fun print_calculation false _ _ = () - | print_calculation true ctxt calc = Pretty.writeln - (ProofContext.pretty_fact ctxt (ProofContext.full_name ctxt (Binding.name calculationN), calc)); +fun maintain_calculation int final calc state = + let + val state' = put_calculation (SOME calc) state; + val ctxt' = Proof.context_of state'; + val _ = + if int then + Pretty.writeln + (ProofContext.pretty_fact ctxt' + (ProofContext.full_name ctxt' (Binding.name calculationN), calc)) + else (); + in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end; (* also and finally *) -val get_rules = #1 o CalculationData.get o Context.Proof o Proof.context_of; +val get_rules = #1 o Data.get o Context.Proof o Proof.context_of; fun calculate prep_rules final raw_rules int state = let val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of; val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl); - fun projection ths th = Library.exists (Library.curry eq_prop th) ths; + fun projection ths th = exists (curry eq_prop th) ths; val opt_rules = Option.map (prep_rules state) raw_rules; fun combine ths = @@ -141,11 +145,12 @@ (case get_calculation state of NONE => (true, Seq.single facts) | SOME calc => (false, Seq.map single (combine (calc @ facts)))); + + val _ = initial andalso final andalso error "No calculation yet"; + val _ = initial andalso is_some opt_rules andalso + error "Initial calculation -- no rules to be given"; in - err_if (initial andalso final) "No calculation yet"; - err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given"; - calculations |> Seq.map (fn calc => (print_calculation int (Proof.context_of state) calc; - state |> maintain_calculation final calc)) + calculations |> Seq.map (fn calc => maintain_calculation int final calc state) end; val also = calculate (K I) false; @@ -164,11 +169,8 @@ NONE => (true, []) | SOME thms => (false, thms)); val calc = thms @ facts; - in - err_if (initial andalso final) "No calculation yet"; - print_calculation int (Proof.context_of state) calc; - state |> maintain_calculation final calc - end; + val _ = initial andalso final andalso error "No calculation yet"; + in maintain_calculation int final calc state end; val moreover = collect false; val ultimately = collect true; diff -r 8f9f3d61ca8c -r d03b57457421 src/Pure/PIDE/state.scala --- a/src/Pure/PIDE/state.scala Fri May 21 17:16:16 2010 +0200 +++ b/src/Pure/PIDE/state.scala Fri May 21 23:21:40 2010 +0200 @@ -74,7 +74,7 @@ { val changed: State = message match { - case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) => + case XML.Elem(Markup.STATUS, _, elems) => (this /: elems)((state, elem) => elem match { case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED) diff -r 8f9f3d61ca8c -r d03b57457421 src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Fri May 21 17:16:16 2010 +0200 +++ b/src/Pure/System/isabelle_process.scala Fri May 21 23:21:40 2010 +0200 @@ -84,7 +84,7 @@ class Result(val kind: Kind.Value, val props: List[(String, String)], val body: List[XML.Tree]) { - def message = XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(kind)) :: props, body) + def message = XML.Elem(Kind.markup(kind), props, body) override def toString: String = { diff -r 8f9f3d61ca8c -r d03b57457421 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Fri May 21 17:16:16 2010 +0200 +++ b/src/Pure/System/session.scala Fri May 21 23:21:40 2010 +0200 @@ -104,7 +104,7 @@ def bad_result(result: Isabelle_Process.Result) { - System.err.println("Ignoring prover result: " + result) + System.err.println("Ignoring prover result: " + result.message.toString) } def handle_result(result: Isabelle_Process.Result) diff -r 8f9f3d61ca8c -r d03b57457421 src/Pure/build-jars diff -r 8f9f3d61ca8c -r d03b57457421 src/Pure/library.scala --- a/src/Pure/library.scala Fri May 21 17:16:16 2010 +0200 +++ b/src/Pure/library.scala Fri May 21 23:21:40 2010 +0200 @@ -17,6 +17,14 @@ object Library { + /* partial functions */ + + def undefined[A, B] = new PartialFunction[A, B] { + def apply(x: A): B = throw new NoSuchElementException("undefined") + def isDefinedAt(x: A) = false + } + + /* separate */ def separate[A](s: A, list: List[A]): List[A] = @@ -94,27 +102,27 @@ /* zoom box */ - def zoom_box(apply_factor: Int => Unit) = - new ComboBox( - List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")) { - val Factor = "([0-9]+)%?"r - def reset(): Int = { selection.index = 3; 100 } + class Zoom_Box(apply_factor: Int => Unit) extends ComboBox[String]( + List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")) + { + val Factor = "([0-9]+)%?"r + def parse(text: String): Int = + text match { + case Factor(s) => + val i = Integer.parseInt(s) + if (10 <= i && i <= 1000) i else 100 + case _ => 100 + } + def print(i: Int): String = i.toString + "%" - reactions += { - case SelectionChanged(_) => - val factor = - selection.item match { - case Factor(s) => - val i = Integer.parseInt(s) - if (10 <= i && i <= 1000) i else reset() - case _ => reset() - } - apply_factor(factor) - } - reset() - listenTo(selection) - makeEditable() + makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x)) + reactions += { + case SelectionChanged(_) => apply_factor(parse(selection.item)) } + listenTo(selection) + selection.index = 3 + prototypeDisplayValue = Some("00000%") + } /* timing */ diff -r 8f9f3d61ca8c -r d03b57457421 src/Tools/jEdit/dist-template/etc/isabelle-jedit.css --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css Fri May 21 23:21:40 2010 +0200 @@ -0,0 +1,13 @@ +/* additional style file for Isabelle/jEdit output */ + +pre.message { margin-top: 0.3ex; background-color: #F0F0F0; } + +.writeln { } +.priority { } +.tracing { background-color: #EAF8FF; } +.warning { background-color: #EEE8AA; } +.error { background-color: #FFC1C1; } +.debug { background-color: #FFE4E1; } + +.hilite { background-color: #FFFACD; } + diff -r 8f9f3d61ca8c -r d03b57457421 src/Tools/jEdit/src/jedit/html_panel.scala --- a/src/Tools/jEdit/src/jedit/html_panel.scala Fri May 21 17:16:16 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala Fri May 21 23:21:40 2010 +0200 @@ -37,18 +37,17 @@ } -class HTML_Panel( - system: Isabelle_System, - initial_font_size: Int, - handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel +class HTML_Panel(system: Isabelle_System, initial_font_size: Int) extends HtmlPanel { - // global logging + /** Lobo setup **/ + + /* global logging */ + Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING) - /* Lobo setup */ + /* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */ - // pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize val screen_resolution = if (GraphicsEnvironment.isHeadless()) 72 else Toolkit.getDefaultToolkit().getScreenResolution() @@ -57,11 +56,15 @@ def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96 + /* contexts and event handling */ + + protected val handler: PartialFunction[HTML_Panel.Event, Unit] = Library.undefined + private val ucontext = new SimpleUserAgentContext private val rcontext = new SimpleHtmlRendererContext(this, ucontext) { private def handle(event: HTML_Panel.Event): Boolean = - if (handler != null && handler.isDefinedAt(event)) { handler(event); true } + if (handler.isDefinedAt(event)) { handler(event); true } else false override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean = @@ -90,7 +93,9 @@