equal
deleted
inserted
replaced
15 /* self-thread */ |
15 /* self-thread */ |
16 |
16 |
17 def self: Isabelle_Thread = |
17 def self: Isabelle_Thread = |
18 Thread.currentThread match { |
18 Thread.currentThread match { |
19 case thread: Isabelle_Thread => thread |
19 case thread: Isabelle_Thread => thread |
20 case _ => error("Isabelle-specific thread required") |
20 case thread => error("Isabelle-specific thread required: " + thread) |
21 } |
21 } |
22 |
22 |
23 def check_self: Boolean = |
23 def check_self: Boolean = |
24 Thread.currentThread.isInstanceOf[Isabelle_Thread] |
24 Thread.currentThread.isInstanceOf[Isabelle_Thread] |
25 |
25 |